# Project State Updated: 2026-10-05 **`v0.8.0` is the published release.** The note is [`docs/releases/v0.8.md`](docs/releases/v0.8.md), and the `v0.8.0` tag with its GitHub Release — not this file and not the note — is the canonical publication record. **The toolchain is Lean v4.33.0 as of 2026-08-31, bumped in its own branch and merged.** Mathlib `db584cd6`, with PFR `7d6404b7` and Foundation `30a16ffa` re-pinned to revisions that resolve against it, replacing `v4.31.0` and `fabf563a`. It buys one thing: `Causalean` is on v4.33.0, so depending on it for the d-separation the causal layer lacks becomes a choice to cost rather than a second migration. Proofs changed and statements did not — 262 graded signatures and 1703 public names unchanged, the axiom audit covering the same 2847 declarations name for name against the pre-migration tree, and every one of the 31 statement-level differences classified: a Mathlib class rename, six `deriving Fintype` instances written out because the upstream handler does not elaborate at this revision, two `linter.checkUnivs` suppressions that refuse a public universe-signature change, and one added private helper. The evidence, the four `by`-block adjudications a textual check cannot settle, and what is owed back are in [`toolchain-v4330-migration.md`](docs/provenance/toolchain-v4330-migration.md). **One module-system behaviour to know before writing a file that imports only atlas modules.** Instance synthesis does not reliably reach an instance that the import graph reaches only through several `public import` hops, even though the declaration resolves by name. `Fintype (Fin 4 × Fin 4)` fails in `Examples/Oversight/JointObservationRegistry.lean` with the atlas imports alone and succeeds the moment `Mathlib.Data.Fintype.Prod` is imported directly; re-checked 2026-09-15 and still reproducible. `![...]` vector notation has the same shape of failure under some chains. The fix per file is the direct Mathlib import naming the instance's home module — relying on transitivity the way plain `import` allowed is what breaks, and it breaks silently. **On `main` since `v0.8.0`, unreleased.** The work since `a65e32f` arrived as one squashed change on 2026-10-01. What it adds, by cluster: - **New clusters** (module counts against `v0.8.0`): Sovereignty 0 → 50 — Pauly, Goranko-Jamroga-Turrini, Peleg's constitutions and societies, the concurrent game frame, Wooldridge and van der Hoek's AATS, the governance bridges, and the cognitive-sovereignty obligation with its open items; LinearSystems 0 → 7; Decision 0 → 5; Goodhart 0 → 5; Composition 0 → 2. - **Extended clusters**: Wireheading 7 → 19 (Ring and Orseau's delusion box and agent equations, the self-modifiable agent, the corrupt-reward MDP's Theorem 11, goal preservation and value reinforcement learning, each graded against print); Knowledge 10 → 14; Causal 15 → 18; Compositional 10 → 13; Verification 2 → 5; Combinatorics 1 → 4; Fairness 1 → 3; and single modules in Analysis, Control, Oversight, Preference and Order. `Examples/` 156 → 275. - **Practitioner checkers**: `atlas-check` goes from five kinds to fourteen. The narrative of how each of these arrived — what was retracted, what was regraded, which costings were wrong — is in [`docs/releases/unreleased.md`](docs/releases/unreleased.md), the draft of the next release note. **Current figures, as of 2026-10-05** (each is computed by the script named; the script, not this file, is the authority): - Lean 637 files, 182,419 lines; public API pin 2,789 names (`check_public_api.py`); registry results 144. - Statement coverage: 28 sources, 300 `Yes` / 17 `Partial` / 208 `No` / 41 `Beyond` (`check_coverage_audit.py`). - Scope debt: 4 owed cells, each costed — Everitt's Definition 17 and Theorem 18, Turner and Tadepalli's A.12 and A.13 (`check_scope_owed.py`). - Witness debt: 3 of 2,696 pinned theorems ungrounded, 2 of them provably unwitnessable; 31 reach no `Examples/` application (`check_witness_debt.py`). - Axioms: everything within `{propext, Classical.choice, Quot.sound}` (`check_print_axioms.py`, `axiom-audit`). - Declarations recorded in the registry: **379** (claim-row WRAPPER **14** / BRIDGE **6**). - Results stating a source claim: **49**; recording a formalization only: **95** (**86** on the public root import). - AI-system bridges (`BRIDGE` declarations): **37**: **30** interpretation-reviewed, **7** statement-reviewed only. Source-claim rows with a reviewed AI interpretation: **3**; statement-reviewed only: **1** (a row-level flag, a different unit). - Open conjectures: **3** of **11** recorded; the ledger also holds **6** determine-problem targets. Problems the atlas cannot state carry no row at all and are recorded against their source directory, so this line does not count them; a resolved row states which printed clause it covers, and one of them (CONJ-003) is true only because its class is empty. - Claim results with statement-match (`EXACT`/`EQUIVALENT`): **16**; with `RELATED`-only formalization: **9**. Counts are claim rows, not records: an artifact row's grade is on the row and never in this number. - Rows carrying atlas Lean: **111** (**24** of them claim rows); catalogued candidate leads: **5**. - Package version: **`0.8.0`** (`lakefile.toml`, cross-checked against `CITATION.cff`). - Latest recorded release note: [`docs/releases/v0.8.md`](docs/releases/v0.8.md). - Published releases are the repository's git tags / GitHub Releases — that list, not this file, is the canonical published set. ## Where the history lives This file records the present. Completed work stays where it can be audited, and is not duplicated here — a second copy of a finished decision is a copy that goes stale without anyone noticing. - **Releases and what each shipped** — [`docs/releases/`](docs/releases/): [v0.1](docs/releases/v0.1.md) (published baseline, immutable audit), [v0.2](docs/releases/v0.2.md) (logic surface, first reviewed bridges), [v0.3](docs/releases/v0.3.md), [v0.4](docs/releases/v0.4.md), [v0.5](docs/releases/v0.5.md) (compositional / wireheading / preference increment, then the workbench-model and process release), and [v0.5.1](docs/releases/v0.5.1.md) (conjecture-ledger maintenance), and [v0.6](docs/releases/v0.6.md) (knowability kernel, Breuer core, BY-044, public page), and [v0.7](docs/releases/v0.7.md) (Wolpert at print scope, the probability substrate, the first domain joint, and a runnable kernel). - **Reproduction, triage and search evidence** — [`docs/provenance/`](docs/provenance/), including the durable residual-gap record [`a1-a3-b1-b3-b7-reverification.md`](docs/provenance/a1-a3-b1-b3-b7-reverification.md) and its stop rules. - **Reviewed AI-system bridges** — [`docs/interpretation-reviews/`](docs/interpretation-reviews/): BY-012 ([`review-by-012-agentbehavior.md`](docs/interpretation-reviews/review-by-012-agentbehavior.md)) and BY-033 ([`ct3-robot-review-package.md`](docs/interpretation-reviews/ct3-robot-review-package.md)), both `REVIEWED` on 2026-07-19, and BY-004 ([`review-oversight-varietybound.md`](docs/interpretation-reviews/review-oversight-varietybound.md)) `REVIEWED` on 2026-08-17, scoped to `Oversight.not_forces_of_card_lt` and not to Ashby's law in general. BY-044 ([`review-by-044-selfawareness.md`](docs/interpretation-reviews/review-by-044-selfawareness.md)) is `STATEMENT_REVIEWED` on 2026-08-12: the encoded statement is accepted, the AI-system interpretation is withheld because none has been proposed. - **Unreviewed AI-system bridges** — [`docs/interpretation-reviews/README.md`](docs/interpretation-reviews/README.md) is the register: **37 bridges, all signed on 2026-10-03/04: 30 `REVIEWED`, 7 `STATEMENT_REVIEWED`**, one review file each. The label is per **declaration** (`review_status` + `review` on the `BRIDGE` entry), not per row — a row is too wide a unit, since `LAND-SOV-AUTH-001` alone owns four bridges about three different things. `validate_registry.py` enforces the lifecycle, the record shape, and that the evidence file exists. - **What is formalized and how it is graded** — [`registry.yaml`](registry.yaml) and the generated [formalization status](docs/status/formalization-status.md) and [by-area index](docs/status/by-area.md). - **Since `v0.8.0`, unreleased** — [`docs/releases/unreleased.md`](docs/releases/unreleased.md). - **Everything else** — git history and the release tags. ## Current work - `v0.8.0` is the latest published release; the next release note is being drafted in [`docs/releases/unreleased.md`](docs/releases/unreleased.md). - Published release history is in [`docs/releases/`](docs/releases/); the notes that used to sit in this section are kept verbatim at the end of `unreleased.md`. - **Planned for `v0.9`: the root import stops growing by default** (recorded 2026-10-05, from an external review of PR #72). The upgrade takes `AISafetyAtlas.lean` from 83 to 251 imports, 20 to 107 of them `Examples/` modules, and the public API pin from 1,836 to 2,789 names (as of 2026-10-05). That works against [`lean-public-api.md`](docs/agent/policy/lean-public-api.md)'s "small stable facade", and `Examples/` are not API yet `import AISafetyAtlas` still pays for them. The rule to adopt: the root is a deliberately small set of canonical primitives and facades; each cluster gets its own entry point (`AISafetyAtlas.Control`, `.Sovereignty`, `.Causal`, `.Decision`, `.Verification`, …); `Examples/` stay off the root unless they are shared infrastructure. Constraint: the generators find modules through the root, with off-root material listed in `scripts/lean_build_targets.txt`, so the split must move them to the per-cluster roots in the same change. Its own PR, not part of #72. ## Blocked - **Public GitHub issue queue (R6-11):** opening issues is maintainer-facing; drafts live in `docs/guide/contributor-tasks.md`. Agents do not open issues without authorization. ## Human review needed - **Tag assignments** (`parsimony`): every registry row — claim and artifact alike — now carries one or more areas from the shared `tag` vocabulary. The vocabulary is validated, but which areas a result belongs to was a judgement call and has not been reviewed. - **Conjecture admission**: whether a proposed conjecture is worth recording is deliberately not automated. See [conjectures](docs/guide/conjectures.md). - Reviewed bridges to date are listed under *Where the history lives*; no bridge is awaiting review. - **The squashed upgrade from `a65e32f`**: work written between 2026-09-08 and 2026-10-01, much of it read by no human before it reached `main` as one squash-merged PR. Two parts deserve separate attention: the witness-debt campaign, which touches `Examples/` and no library statement, **and** four bridge changes on the evening of 2026-09-14 adding roughly 1,366 lines of new public library declarations. - **37 `BRIDGE` declarations, all signed by the maintainer on 2026-10-03/04**: 30 `REVIEWED`, 7 `STATEMENT_REVIEWED` (the statement accepted, the AI-safety reading withheld). Before signing, every allowed claim was narrowed to what its Lean statement proves, after an external review on PR #72 found two too broad; the narrowing reached the review files, the module docstrings and the registry `application` fields. The label is per declaration, so artifact rows show it even though `ai_interpretation_status` is forbidden there. - **Six of those are new on 2026-09-16 and they are the governance ones**, over a cluster that had four. The sovereignty layer carries 462 public theorems across 36 modules and 30 registry rows — `formal-power-proposal-triage.md` closes 63 of the proposal's 64 results with no row left `SUBSTRATE` — and almost all of its AI-safety reading lived in registry *prose*, inside the `application` field of a `NEW_PROOF` declaration. Prose in an application field is not layer 3. The six are: an undetectable norm is unenforceable (`Sovereignty.Enforcement`, which is the edge between `Deontic` and `Auditability` — two modules that existed and did not import each other); obedience to delivered commands is not an advance guarantee of delivery (signed statement-only: the principal can observe and retry); passing every check is not operability; an attestation is not its claim; two properties need not imply each other; and power over a party need not be power over a matter. Each is witnessed in `Examples/Sovereignty/Governance.lean`, with the escape exhibited wherever one exists — the same rule under a monitor that sees the act *is* enforceable, and a catalogue one policy does serve is operable. Provenance: `docs/provenance/governance-bridges.md`. All six are signed, five `REVIEWED` and the shutdown one `STATEMENT_REVIEWED`. ## Next three tasks These three predate the 2026-09-10 integration and are unchanged by it; the branch's own open items are in the paragraphs above and are not scheduled here. 1. Review the A1–A3/B1–B3/B7 statement maps and residual-gap record before proposing any relationship change. 2. If a named consumer requires paper depth, choose one coherent package: B2 modification-independence/all-times derivation or B3 stochastic CRMDP with extrema derived from finiteness. 3. Keep B7 Conjecture 9 predicate-only and Proposition 10 blocked until genuine resource-bounded complexity infrastructure exists.