← All status

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.