lean

V15 readiness ledger — Cross-Calculus Atlas

Date: 2026-07-22

Status: released 2026-07-24

V15 records checked mappings for selected edges from GT, Execution Custody, and Continuity Admission, preserving the native judgment indices, local countermodels, and exact receipts required by those edges. It includes an exact-receipt anti-minting result and a held-out partial StaticRole instance. It does not establish a shared bridge algebra, generic frontier composition, generic ownership, generic context transport, or a universal calculus.

This ledger is rooted at the operator-ratified public integration commit 1f0e0208584e0f61fe49353dd0fc6b4775e22e00, tree d2424b28a932c68027ec7bb0bbebd1e169221b99, parent 8113544cd7e8420d14b3f02c2325873aef2ac15b. The final candidate commit, tree, and parent are recorded in the separately committed verification receipt and operator handoff, avoiding a self-referential Git object.

Ratified local chain

Gate Commit Tree Parent
exact public transfer d1e2d18ffc6e27365ec890a6ae2439c87688b350 fbd5a31ec5e2432759db45d2359c3e3f74198b52 9dca58f4587a4a4f5b724662b176af8de3040c04
transfer ratification record 8bfa849693b3795b6c7236161baaa54c9f1f82f2 d47f0f779d05031e8ae61937cfb1e1b5e03800e2 d1e2d18ffc6e27365ec890a6ae2439c87688b350
exact Continuity rename 46e7a9aa5944fcc8826445c74ec08e1aa2dcb630 e27bc3174d3e9bd2d6f843d871a823c2b036674b 8bfa849693b3795b6c7236161baaa54c9f1f82f2
dependency integration 0b513fa184c12a10c685a6d13e45d085cd19499b 39ddfae2d420961cbe4809abe1ed1c3a4073e112 46e7a9aa5944fcc8826445c74ec08e1aa2dcb630
Track A reconciliation 05b4dff4df27bf69a9e3552498bc2ef92bed3242 8b2ebf8d9a8b715ce932e61d52e173f0d9f6f900 0b513fa184c12a10c685a6d13e45d085cd19499b
cleanup and public index 76d568a78d1611420ea765901ae679a9bc16ee84 3167a74fe0c08a24e14c8de5d87ff9a01f413201 05b4dff4df27bf69a9e3552498bc2ef92bed3242
namespace-terminator correction 8113544cd7e8420d14b3f02c2325873aef2ac15b 68ba6198a56d66c81592fdef882b2f9ff805c037 76d568a78d1611420ea765901ae679a9bc16ee84
integration verification receipt 1f0e0208584e0f61fe49353dd0fc6b4775e22e00 d2424b28a932c68027ec7bb0bbebd1e169221b99 8113544cd7e8420d14b3f02c2325873aef2ac15b
qualification hostile audit 247e5d002f40288c06452b9f6913ccb967c9655e f0ff26c2a2bd0718096a1b3bd3b9363a30c1a704 1f0e0208584e0f61fe49353dd0fc6b4775e22e00
release-candidate metadata df37e95d558035f91dcd0dbed48cf9f14fda5b28 83fdd97ee0f376a1e60b0836fc18593c82eec8e7 247e5d002f40288c06452b9f6913ccb967c9655e

Source and campaign pins

The private/public transfer manifest remains SHA-256 05a29867a8c9c24996f9a1b975749a61379f32b5b8cdebc9a1100504147d6268; the normalized custody manifest remains SHA-256 471ec4b52bdcb163dafa8eab671e5f26b9401351ff4da9908db0ab8e214b5e1d.

Continuity rename identity

Someone crossed to the single authoritative public implementation Continuity.Admission. The correspondence manifest SHA-256 is 3aafc4eceb0e96899772bb5824bbac3c999ede5e9355786982e3761a2071fabb. It covers 1,005 declarations and checks old/new fully qualified names, normalized types, proof values, and axiom footprints. The claim remains identity-bound continuity admission on the reachable fragment; it does not establish authenticated identity, durable revocation, substrate rebinding, retained route history, typed refusal, obligations, or operational-Continuity correspondence.

Track A freeze

Inquiry and Preparation remain byte-exact at private freeze commit cfeffc950e795752ad1928a314890185c0cda723, tree 4d9de55c0d19f3984dc486ac124b2e4f2a7e1e11, custody closure de32412a7a29fbc98273c08747256ca9d319cfbd. Six Lean blobs and three boundary records reproduce. Their 102 theorems are independently scoped: Inquiry 74 and Preparation 28; 83 are axiom-free and 19 use only propext. They are comparison-only neighbors outside the frozen PJ primary surface.

Compiled declaration and axiom footprint

docs/V15-PUBLIC-DECLARATION-FOOTPRINT.json is a deterministic census of the V15-owned Continuity Admission, StaticRole, and PJ declaration surfaces. Existing GT, Execution Custody, and Admissibility declarations retain their separate public receipts.

Surface Declarations Theorems Axiom-free [propext]
Continuity Admission 1,005 281 868 137
StaticRole R0–R3 1,010 445 992 18
PJ Atlas 591 227 571 20
Total 2,606 953 2,431 175

The total contains zero [Quot.sound], zero [Classical.choice], and zero mixed/other entries. These classifications are inherited; qualification did not rewrite proofs to reduce them.

The hostile-fixture policy counts declarations in the Continuity hostile qualification module, StaticRole Countermodels modules, and the exact PJ hostile/boundary modules: 14 + 460 + 261 = 735 compiled declarations. The public hostile ledger directly maps the twelve required representative collapse attacks to reproduced witnesses.

StaticRole remains exactly R0–R3 with no R4. PJ remains ATLAS, including FRONTIER-NOT-COMPOSITIONAL, NO-USEFUL-OWNERSHIP-COMMONALITY, CONTEXT-TRANSPORT-NOT-GENERIC, and ONLY-DOMAIN-SPECIFIC-RESIDUAL-THEORIES.

Candidate metadata and paths

The candidate version is 15.0.0 and the conservative title is V15 — Cross-Calculus Atlas. CITATION.cff retains the concept DOI but sets no release date and no unminted version DOI. The current published v14 tag and release remain unchanged: annotated tag object 595b632f65b926d5430a2ff7ff031b502a26cfe0, peeled commit ff491b808ebeab2a132d9ade46d234cf85dcfbe9, tree 72cba07e35588e9f67c252b0bd92cf0523ab178f, version DOI 10.5281/zenodo.21435270, concept DOI 10.5281/zenodo.20369489.

The complete campaign allowlist is docs/V15-RELEASE-CANDIDATE-PATHS.tsv. No formal source, custody registry, target registry, stable-root list, v14 surface, or generated custody aggregate is changed by qualification.

Qualification commands

The candidate receipt records the exit status of:

lake build V15Integration
lake build V15IntegrationQualification
lake build CalculiStable CalculiScratch CalculiAll Calculi
python3 scripts/formalization_audit.py check --skip-external --skip-footprints
lake env lean <each of the seven V15 qualification leaves>
python3 scripts/check-v15-continuity-rename.py
python3 scripts/check-v15-integration.py
python3 scripts/check-v15-public-qualification.py
bash scripts/audit-axioms.sh
bash scripts/audit-native-decide.sh
bash scripts/check-mathlib-pin.sh
bash scripts/check-custody-classes.sh
bash scripts/check-mathlib-free-targets.sh
git diff --check

Exact non-claims and remaining actions

V15 is not a shared bridge algebra, generic frontier composition law, generic ownership theory, generic context transport, universal calculus, Planet, Archipelago, complete theory of machine judgment, JCP implementation, or operational AG/NQ realization. Receipt fibers and residual theories remain local. StaticRole is a qualified held-out partial instance, not an R4 claim.

Only the operator may ratify the local candidate and later, in separately authorized actions, push, tag, create a GitHub release, assign release dates, mint a version DOI, or publish. No push, tag, mint, publication, or release occurred during this campaign.

This site is open source. Improve this page.