Repository navigation
Logbook September 2026
Week of Monday 31st (continued) — Inversion coverage of the Lean events is completed, closing the gap the earlier gates exposed.
Every event now has its inversion covered, after a mandate freezing what coverage means. Merged #65.
Week of Monday 31st August, weekend — Verification tooling dominates. The Lean checks are made total over everything that exists instead of a hand-kept list, the proposer-is-not-an-assent rule goes through planning and implementation, verified trace corpora are exported, and the simulator is re-bound to the single membership model. Money custody is implemented and the preview is published.
The axiom gate now discovers every declaration and fails closed on unknown kinds, with ownership resolved from the compiled output. Inversions resolve by unqualified name and the coverage instruments agree (#79, #88). Prop and Bool mirrors with correspondence proofs and a mandatory checker are added, and verified Lean trace corpora are exported (#87).
A proposer's signature no longer counts as an assent. The planning contract, witness guards hardened against vacuous passes, and a fenced witness oracle precede the change (#80). The simulator is re-bound onto one membership, preserves substrate string keys in every control, and binds caller identity through decode, validate and replay.
Money custody with four arms is implemented (#95), and the simulator is re-bound to the merged Lean model (#94) with observable geometry enforcement and both rings expanding on a pannable canvas. The simulator is now published through the pull request preview and docs site, bound to the PR head and restricted to same-repository runs. The mirror checker driver, import reach, and its repair rounds merge as #89.