Status: released 2026-07-24.
Candidate pin: commit 5232a697b6f0cfd628e01876b7b19efb9e319b3e, tree
510f7c42a0edad406a7762cc11c0e7f0ee554687, parent
62d118a6ede996d4b3e0351d5db3ae7e3aa04f07. The version DOI is minted by the
GitHub release creation and recorded from Zenodo afterward, never guessed
here.
Subtitle: Receipt-indexed correspondence without a shared bridge algebra.
V15 records checked, source-preserving mappings for selected edges from Governed Transport, Execution Custody, and Continuity Admission. The adapters retain the judgment indices, local countermodels, and receipt-bound entitlement required by those edges. V15 also includes an exact-receipt anti-minting result and a held-out partial StaticRole instance.
“Receipt” here means the bridge-specific semantic evidence family indexed by
its source and target. It does not imply a digital signature, hash chain,
zero-knowledge proof, or other cryptographic commitment. The anti-minting
result specifically blocks receipt-free construction of source-relative
EntitledFrom at an exactly refuted index pair; it is not a theorem about
every form of evidence, authority, spend, discharge, or closure.
The classification is ATLAS. V15 does not establish a shared bridge algebra,
generic frontier composition, generic ownership, generic context transport,
or a universal calculus. It makes no runtime-conformance, JCP-implementation,
or operational AG/NQ realization claim.
Primary public evidence:
V15-PUBLIC-INDEX.md;V15-PUBLIC-HOSTILE-AUDIT_2026-07-22.md;V15-INTEGRATION-VERIFICATION-RECEIPT_2026-07-22.md;V15-READINESS-LEDGER.md; andV15-CANDIDATE-VERIFICATION-RECEIPT_2026-07-22.md.PJ maps selected qualified seams and preserves their native indices, receipts,
positive carries, and countermodels. It is called an Atlas because those
checked correspondences do not create a common algebra: generic frontier
composition, ownership commonality, and context transport failed, while
residual theories remained domain-specific. Those are negative scientific
results, not unfinished implementation work. The
public index records which edges are mapped and which
source-local laws are omitted.
An IndexedJudgmentBridge is not presented as a generic categorical object:
it is one oriented, evidence-bearing rule with independently indexed source
and target judgments, an instance-owned receipt family, and a carry operation.
No generic identity or composition field exists in PJ.
Exact-receipt anti-minting is non-definitional but adapter-local. Independent target truth or a bare bridge inhabitant does not create source-relative entitlement when the exact native receipt fiber is empty. The result is not a generic law that qualifies arbitrary bridges, and PJ itself does not supply bridge lawfulness.
StaticRole contains four bounded structural levels: R0 external center-relative roles, R1 internal role encoding, R2 coherent prospective de se reference transport, and R3 structural functional uptake. R3 is independent of output correctness and does not establish consciousness, phenomenology, successful prediction or agency, psychology, neural implementation, temporal passage, or metaphysical personal identity. Its PJ mapping is partial because the dependence structure remains local to StaticRole; no R4 exists.
The GT adapter preserves exact route-bearing translation separately from target-local reliance. It establishes no runtime or deployment correspondence. Execution Custody likewise keeps attempt permission, commit permission, commit attempt, succeeded/refused outcome, and unknown outcome distinct; authorization does not imply an attempt, commit, or observed effect.
Continuity.Admission is the one authoritative public implementation. The
frozen someone/ directory and the transferred Someone qualification/PJ
campaign records preserve the private excavation name and the state of each
historical gate. Their private-era Someone.lean references identify the
frozen source object and are not current public module links. The
historical-name note records
the exact rename; the final PJ operator record, rather than earlier candidate
classification documents, governs the ATLAS verdict.
The public source is under LeanProofs/ and formalization/. The repository
pins Lean 4.29.0 (leanprover/lean4:v4.29.0) and builds the v15 public surface
with:
lake build V15Integration
lake build V15IntegrationQualification
GitHub Pages renders the root README.md from main. The Pages body and
response headers should be verified independently after a push. A green
build or deployed page does not by itself create a tag, GitHub release,
Zenodo deposit, or runtime-conformance claim.