lean

V15 public integration verification receipt

Date: 2026-07-22

Disposition: READY-FOR-V15-INTEGRATION-RATIFICATION

The ratified public transfer is integrated behind canonical, non-default public-evidence targets. Someone has crossed to Continuity.Admission with its declaration, proof-value, and axiom correspondence preserved. StaticRole remains closed at R3. PJ remains exactly ATLAS: a faithful cross-calculus atlas, not a shared algebra or universal calculus.

No push, tag, mint, publication, release, remote configuration, remote-branch change, stable-root promotion, default-target change, or release-metadata change occurred.

Transfer base

The transfer object is an ancestor of this receipt. Its tree, frozen campaign manifests, final-verdict record, and existing public LeanProofs source calculi reproduce exactly.

Integration commits and exact paths

1. Transfer ratification

2. Exact Continuity rename

The correspondence covers 1,005 declarations: fully qualified names, kinds, normalized theorem/type expressions, proof values, and axiom footprints. There is no duplicate authoritative Someone implementation.

3. Formal dependency integration

The canonical targets are V15Integration and V15IntegrationQualification. They are explicit, Mathlib-free, public-evidence targets and are not stable or release aggregates.

4. Track A reconciliation

The private Track A freeze remains commit cfeffc950e795752ad1928a314890185c0cda723, tree 4d9de55c0d19f3984dc486ac124b2e4f2a7e1e11. Its six Lean blobs and three boundary-record blobs reproduce exactly. Inquiry and Preparation are independent comparison-only neighbors outside the frozen PJ primary surface.

5. Cleanup and public index

The two temporary transfer targets were removed only after their canonical replacements were green. All transferred formal sources remain owned.

Exact namespace-terminator correction

The full source-identity checker found that the renamed adapter had relied on Lean’s end-of-file namespace closure rather than retaining its explicit final end line. This commit restores that exact namespace-adjusted terminator. The module built before and after; its declaration, theorem, proof-value, and axiom surfaces are identical. The correction is isolated rather than hidden in cleanup or history rewriting.

Manifest and verdict verification

The five frozen declaration-manifest SHA-256 digests are:

Manifest SHA-256
Continuity historical declaration manifest 521c437be1d7f2ac93d0dfded7b368158a339cad8ee004ffb29d41120848c3b9
PJ-A be2b092ed2e08e948858e7d7a6ae77893b1baf36b6d95cb58050401cfbe2955a
PJ-B-prime c7544b561271ca64f0c15d8f7c9a980b7cf7eb3da8ce020f0aece3c3aebfebc4
PJ-C-prime 09c203d95157afb0ef379668f64753a9e74fb22c7e2387c8efde7c5e5d4821ab
PJ-D-prime 5b4947101d4610fa86c536449e4eba399b601cf4c1b3cb396579d668b39f6e6a

The integrated checker verifies all four PJ dumps against their frozen manifests after only the authorized namespace correspondence: 1,950 cumulative manifest declarations, including 74 cumulative axiom-bearing entries. Source text for every declaration-bearing renamed PJ file is the exact transfer source after the authorized rename substitutions. Unchanged public source calculi remain byte-identical to the transfer base.

The final PJ operator-verdict record remains SHA-256 3efad909f66b2caed45e57606c3c879ad877e902606d4046e057eff7942002aa and says RATIFY-PJ-D: ATLAS. It retains:

No rejected PJ frontier directory and no StaticRole R4 path exists.

Verification commands

Each bare command below exited zero in the indicated repository:

/home/jbeck/git/lean$ lake build V15Integration
/home/jbeck/git/lean$ lake build V15IntegrationQualification
/home/jbeck/git/skunkworks/formalization$ lake build CalculiStable CalculiScratch CalculiAll Calculi
/home/jbeck/git/skunkworks/formalization$ python3 scripts/formalization_audit.py check --skip-external --skip-footprints
/home/jbeck/git/lean$ lake env lean formalization/Continuity/Admission/Qualification/Campaign.lean
/home/jbeck/git/lean$ lake env lean formalization/StaticRole/Campaign/Qualification.lean
/home/jbeck/git/lean$ lake env lean formalization/StaticRole/Campaign/PhaseThreeQualification.lean
/home/jbeck/git/lean$ lake env lean formalization/PJ/Campaign/TrancheAQualification.lean
/home/jbeck/git/lean$ lake env lean formalization/PJ/Campaign/TrancheBPrimeQualification.lean
/home/jbeck/git/lean$ lake env lean formalization/PJ/Campaign/TrancheCPrimeQualification.lean
/home/jbeck/git/lean$ lake env lean formalization/PJ/Campaign/TrancheDPrimeQualification.lean
/home/jbeck/git/lean$ python3 scripts/check-v15-continuity-rename.py
/home/jbeck/git/lean$ python3 scripts/check-v15-integration.py
/home/jbeck/git/lean$ bash scripts/check-custody-classes.sh
/home/jbeck/git/lean$ bash scripts/check-mathlib-free-targets.sh
/home/jbeck/git/lean$ git diff --check

The Calculi build completed 269 jobs. The formalization audit passed 19 checks. The custody gate closed over 273/273 public Lean sources, and the target gate closed over 28 registered public targets with 273/273 public sources target-owned. Every changed path was inspected.

This receipt’s commit and tree are recorded in the operator-facing handoff; they cannot be embedded in the receipt without making its Git object self-referential. Its exact parent is 8113544cd7e8420d14b3f02c2325873aef2ac15b, and its only paths are this receipt and scripts/check-v15-integration.py.

This site is open source. Improve this page.