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) has begun: S-T2 (memory-index bijection, plus its reachability refinement), S-T3 (provenance authority / anti-poison — the value proof, ratifying the 3 §2d injection-channel [SEED] classifications), the § 10 git↔session decomposition bridge (/open → /close → S-T5 → S-T7 → /lift), and S-T4 (cross-repo ownership totality — the last ranked invariant) all proved over structurally-synthetic snapshots.
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.32.0
- theoremsProved
- 98
- coverageTheorems
- 70
- daoRounds
- 63
- attacksParried
- 341
- attacksLanded
- 2
- openGaps
- 0
- falsifiabilityBlindCertified
- 0
- numeratorCellsMet
- 22
- blindRecertifiedNumeratorCells
- 20
- leanGraphEmitFresh
- 1
- leanGraphEmitRev
- d4a15a762
- leanGraphModality
- domain-graph
- leanGraphDenominator
- 22
- leanGraphCoveragePct
- 0.5454545454545454
- leanGraphVelocity
- 0
- leanGraphGoldenShare
- 0.5454545454545454
- leanGraphAutomatedShare
- 0
- leanGraphMeanDeps
- 14.5
- leanGraphGeneratedFactShare
- 0.3021346469622332
- leanGraphToolchainCurrent
- 1