# v0.7 Release - Prepared: 2026-08-15 - Published: 2026-08-15 to `main`; tag `v0.7.0` - Publication status: **published** — the `v0.7.0` tag is the canonical publication record. Package version: **0.7.0** (`lakefile.toml`, `CITATION.cff`). ## One-paragraph truth A depth release on one source and a structural release on everything else. Wolpert's *Physical limits of inference* is now the largest body of mathematics in the tree — inference devices, weak and strong inference, control, complexity, stochastic devices, and the 2018 physical-knowledge cluster — carried at the source's own quantifiers rather than at convenient specializations, with every finiteness restriction the encoding did not need removed and every place the printed text fails to determine a formal statement recorded as a numbered clash. Supporting that required a probability substrate the atlas did not have: finite mass functions, entropy, mutual information and KL divergence, with Mathlib `PMF`/`Measure` interoperation. Structurally, the release does three things the atlas had never done: it **joins two domains** — `Knowledge.Devices` transports between the knowability kernel and Wolpert's devices, in both directions, without identifying them — it makes the kernel **runnable** by a consumer who cannot read Lean, via `Knowledge.Check` and the `atlas-check` executable, each backed by a Lean theorem that the runner agrees with the proof, and it puts **every domain** under a generated dependency view instead of the two that happened to be under work. Finally, every source backing Lean in the tree was re-checked against its published text, which found and fixed a real citation defect. ## What changed since v0.6.0 - **Wolpert 2008 at print scope.** `AISafetyAtlas.Inference` is now 25 modules: devices, reduced form, weak and strong inference, mimicry, control, inference complexity, stochastic devices, and physical knowledge. Statements are widened where the proof never used the restriction — Theorem 4 with no finiteness on either setup range, Definition 6 over a countable target range, Theorem 7(i) without its universe restriction, `C-hat` over an arbitrary setup range, Definition 10 over countably supported setups of finite entropy. - **The source read as a source, and corrected where it is wrong.** Every row was checked against the LaTeX sources and against the Elsevier article, not only the preprint. Where the printed text does not determine a formal statement, the ambiguity is a numbered clash recording which reading the Lean encodes. Where the printed statement is **false**, it is refuted with a machine-checked countermodel: Corollary 1(ii) of the 2008 paper is false as printed and needs a proper subset the statement omits; in the 2018 preprint, Proposition 12 fails on a four-state countermodel meeting every printed hypothesis, Example 6's sharpness claim does not hold, and Corollary 25's target is inadmissible under its own equation (11). Of the 46 tracked 2008 statements, **42 are `SOURCE-EXACT`**, one is specialized, two are repaired and one is refuted, with none unmechanized. - **A probability substrate.** `FinPMF`, entropy sums, mutual information and KL divergence, with `PMF` and `Measure` interoperation — built because the 2008 and 2018 material needs it. It is *shaped* to be independent of either; nothing outside `Inference` uses it yet, and the non-claims below say so. - **The first joint between domains.** `Knowledge.Devices` transports between `Knowledge.Knowable` and Wolpert inference devices in both directions, under explicit hypotheses, and **deliberately does not identify them** — the non-identification is itself witnessed both ways. - **The kernel became runnable.** `Knowledge.Check` supplies executable checkers with agreement theorems, and `atlas-check` (`Main.lean`) is a command-line tool that decides knowability, coalition coverage and device questions from a JSON model. Twelve checks are asserted to agree with the Lean proofs, plus a scaling guard. - **One scenario that is a job.** `Examples.Oversight.Overseer` runs the transport on an overseer that may reconfigure — one overseer answers every probe yet its report stream is not knowable; the other's report factors through its setup and is refuted at every configuration. - **Navigation for the whole tree.** Dependency views are generated for all thirteen domains, and CI regenerates and diffs them. - **The executable is in the trust scan.** `Main.lean` is covered by the same `sorry` / axiom checks as the library. - **Published numbering, not report numbering.** Everitt, Filan, Daswani and Hutter is cited as the published AGI 2016 **Theorem 12** (the chapter proves nothing and delegates to technical-report Theorem 16). Van Leeuwen and Wiedermann's published chapter reuses the report's numbers for different statements; a collision table records that. Wolpert 2018 has no peer-reviewed version; the registry says so. ## Release inventory The release tree records: - **124** unique Atlas Lean declarations; - **77** results — **49** claim rows and **28** artifact rows; - **86** catalogued sources and **64** formalization records; - **37** results carrying atlas Lean at any grade; of the claim rows, **12** reach `EXACT`/`EQUIVALENT` and **7** are `RELATED`-only (one artifact row, `LAND-SELFMEAS-002`, is also `EQUIVALENT`, so **13** rows in all); - **2** reviewed AI-system bridges and **1** statement-reviewed bridge whose interpretation is withheld; - **1** open conjecture; - **774** public declarations inside the axiom audit. These are inventory and evidence counts, not a completion target. ## Critical non-claims - **No new reviewed bridges.** The count stays at 2 (BY-012, BY-033). Nothing here licenses a claim about a deployed system. - **The knowability kernel and Wolpert's devices are still not the same thing.** `Knowledge.Devices` transports between them under stated hypotheses; the non-identification of `Knowable` with `WeaklyInfers` and with `PhysicallyKnows` is witnessed in both directions and is not withdrawn. - **`atlas-check` decides models, not systems.** A verdict is about the JSON model it was given. The agreement theorems say the runner matches the Lean, not that any model matches a real deployment. - **Wolpert 2018 rests on a preprint.** No published version exists; the atlas reads `arXiv:1711.03499v3`, and this is the only source in the tree where a preprint is the authority. - **BY-033 matches the unrefereed technical report**, not the published chapter, whose Theorem 1 is strictly stronger and carries a regularity hypothesis the report's does not. - **`RELATED` on BY-024 is about row coverage, not transcription depth.** The survey row cites four works; the atlas transcribes Wolpert 2008 in full and the 2018 preprint substantially, and leaves Wolpert 2001 and Devereaux et al. untranscribed. The grade follows from that, and from the presence of repairs, specializations and refutations — not from shallowness. The per-statement record is the accurate instrument. - **The relationship vocabulary cannot express "corrects the source."** `EXACT`/`EQUIVALENT`/`RELATED` assume the source is right and grade fidelity to it. A formalization that is stronger than print in some places, weaker in others, and refutes the source in a third set has no single correct label. This is recorded as a limitation of the vocabulary, not resolved. - **The recorded clashes are not proof gaps.** Each is a place where the printed source does not uniquely determine a formal statement; each records which reading the Lean encodes. - **Resource-bounded complexity is still absent**, which is why Armstrong's Proposition 10 is not formalized and why MAIS-O1 and MAIS-O16 remain not statable against `AISafetyAtlas.Logic.loeb`. - **The depth is not yet vocabulary.** `Inference` is 55% of the library (12,332 of 22,625 lines) and, outside its own subtree and its own examples, has exactly **one** library consumer: `Knowledge.Devices`. The probability substrate it introduced — `FinPMF`, entropy sums, mutual information, KL divergence — has **no** consumer outside `Inference` at all. That is depth on one source, not a shared primitive, and it is recorded here rather than left to be discovered. Making the substrate usable without importing Wolpert is identified work, not done work. - **One joint is not composition.** `Knowledge.Devices` is the first transport between two domains and remains the only one. Seven distinct notions of agent behaviour coexist in the tree — in `Wireheading.CRMDP`, `Wireheading.AgentEquations`, `GoalPreservation`, `GoalPreservationSource`, `Verification.Robot`, `Preference` and `Compositional.Hyperproperties` — with no transports between any of them. ## Objective evidence - `scripts/agent_gate.sh` green: validator regressions, 67 pytest tests, `ty` clean, all generated views regenerate identically. - `lake build` completes (**2932** jobs). The default target is the library alone; `lake build AISafetyAtlas atlas-check` completes (**3640** jobs), and adding the off-root conjecture modules, `lake build AISafetyAtlas atlas-check AISafetyAtlas.Conjectures.Checks`, completes (**3642** jobs). - `scripts/check_print_axioms.py`: **774** declarations within `{propext, Classical.choice, Quot.sound}`. - `scripts/check_public_api.py`: **774** pinned declarations. - `scripts/check_atlas_check.sh`: **12** checks agree with the Lean proofs, and the scaling guard holds. - `scripts/audit_release.py` green. - No `sorry`, no `native_decide`, no `plausible`, and no custom axioms in the tree. - Provenance: [inference devices](../provenance/wolpert-inference-devices.md), [2008 source clashes](../provenance/wolpert-2008-source-clashes.md), [2018 knowledge](../provenance/wolpert-2018-knowledge.md), [statement maps](../provenance/a1-a3-b1-b3-b7-statement-maps.md). ## Citation and publication boundary The published set is the repository's git tags and GitHub Releases. This note describes what the `v0.7.0` tag contains; that tag, not this file, is the canonical record.