Studying
Studying
Operational-axis Lean4 kernel + cross-axis representation research. Axiomatizes qagents operations (git first) with the same kernel + LLM-facts + lake-build architecture as proving/ and accounting/; owns the hub/ guide-rails. T1 (branch-lock exclusion), T3 (worktree divergence detection), T2 (cascade safety) and T4 (adopted-spec promotion discipline + its breach dual, over the index→commit substrate) proved by the /dao coding-v.-testing lane over extracted repo snapshots. The second operational target (axiomatize-llm-ops, the LLM session substrate) proves its ranked invariants, including the git↔session decomposition bridge (/open → /close → /lift), over structurally-synthetic snapshots; the session-substrate theorems themselves are tracked privately and are not enumerated on this public surface (focus-areas § 10 note; ns:studying/252).
Correction ·
Agreement-tier figures withdrawn pending re-verification
What we found. Our own adversarial review lane found leak channels in the cross-axis agreement oracle that classifies our Tier-A/B/C figures. The fan-out agents that are supposed to agree independently could, in principle, see each other's work — so blind agreement was never established for any wave.
What survives. Kernel soundness is unaffected and mechanically re-checked: every lake build, every sorry-free proof still stands. You cannot leak your way into a green build — the encoded work is real. Only the agreement-based confidence is in question.
What is withdrawn. The agreement-based tier counts (proving's Tier-A/B/C and accounting's) are withdrawn — shown as "withheld", restated provisional as of 2026-07-14. Sections-encoded, universe %, sector census and the soundness panels are mechanical and remain.
The schedule. Re-earning a tier means a fresh blind re-slice under the now-closed contracts, not a re-score of the old one. It is sequenced cheapest-first: the operational axis re-attacks first, the financial axis re-slices next, and the textual re-slice is a multi-week program. This notice updates as each axis re-earns its figure.
Diagrams pending (operational kernel)
Workflow views mount in monitoring/ (local-only) via the kit-mount pattern; the /status card carries metrics only.
Metrics
- focusAreaCount
- 10
- toolchain
- leanprover/lean4:v4.34.0
- theoremsProved
- 106
- coverageTheorems
- 78
- daoRounds
- 66
- attacksParried
- 363
- attacksLanded
- 23
- openGaps
- 12
- falsifiabilityBlindCertified
- 0
- numeratorCellsMet
- 22
- blindRecertifiedNumeratorCells
- 18
- leanGraphEmitFresh
- 1
- leanGraphEmitRev
- 76a014e22
- leanGraphEmitInputDigest
- sha256:e2c2670fdddf30bd2a0f46a60b69abd4525ad0c14d321bf4d174845fdbeaabaa
- leanGraphModality
- domain-graph
- leanGraphDenominator
- 22
- leanGraphCoveragePct
- 0.5454545454545454
- leanGraphVelocity
- 0
- leanGraphGoldenShare
- 0.5454545454545454
- leanGraphAutomatedShare
- 0
- leanGraphMeanDeps
- 14.5
- leanGraphGeneratedFactShare
- 0.3021346469622332
- leanGraphToolchainCurrent
- 1