Date: 2026-07-22
Disposition: PASS — bounded Atlas claim preserved
This audit treats integration summaries as untrusted and checks the ratified formal objects, their source pins, public prose, and representative collapse fixtures directly. No proof source was changed by the audit.
scripts/check-v15-continuity-rename.py reproduces the complete
1,005-declaration Someone to Continuity.Admission correspondence,
including normalized theorem expressions, proof values, and axiom classes.cfeffc950e795752ad1928a314890185c0cda723, tree
4d9de55c0d19f3984dc486ac124b2e4f2a7e1e11.9dca58f4587a4a4f5b724662b176af8de3040c04, tree
7e2b27939bafe7a214085112af2777e395b1b94f, blob
961f4d2a1ea7c5d9236338dedf42ded6481d1c3e, SHA-256
13f0f8164ff6c9de6b9cfb05053fc1bed58aeb7d8c3f2289df5d69cb32dd5b7c.The final PJ declaration manifest remains 591 compiled declarations: 571
axiom-free and 20 exactly [propext], with zero Quot.sound,
Classical.choice, mixed, or other footprints. PJ-A’s core contains only the
indexed bridge signature and local entitlement packaging; it supplies no
qualification, owner, authority, custody, spend, frontier, or context law.
The direct A, B-prime, C-prime, and D-prime leaves reproduce. They retain the
adapter-local receipt fibers, target-truth refusal, non-definitional
exact-receipt anti-minting, held-out StaticRole partial instance, and the
Admissibility out-of-sample result. The final operator record remains SHA-256
3efad909f66b2caed45e57606c3c879ad877e902606d4046e057eff7942002aa
and says RATIFY-PJ-D: ATLAS.
The following classifications remain authoritative:
FRONTIER-NOT-COMPOSITIONAL;NO-USEFUL-OWNERSHIP-COMMONALITY;CONTEXT-TRANSPORT-NOT-GENERIC; andONLY-DOMAIN-SPECIFIC-RESIDUAL-THEORIES.| Requested attack | Reproduced public witness | Result |
|---|---|---|
| bridge/target inhabitant without receipt | PJ.Hostile.ExactReceipt.bare_target_truth_does_not_supply_receipt |
target truth remains unentitled |
| target truth without entitlement | PJ.TrancheBPrime.Instances.GovernedTransport.true_target_has_no_exact_route |
exact GT receipt fiber remains empty |
| wrong subject receipt | PJ.TrancheBPrime.Hostile.wrong_subject_remains_not_entitled |
refused at the original subject index |
| wrong context receipt | PJ.TrancheBPrime.Hostile.wrong_context_remains_not_entitled |
refused at the original context index |
| wrong bridge receipt | PJ.TrancheBPrime.Hostile.wrong_native_bridge_remains_not_interchangeable |
native receipt force is not interchangeable |
| frontier record projection | PJ-B-FAST-FALSIFICATION_2026-07-22.md |
rejected; no exploratory frontier module is present |
| owner as empty label | PJ.TrancheCPrime.Ownership.StaticRole.lawful_action_does_not_supply_functional_uptake |
labels do not manufacture an owner or uptake receipt |
| context transport as trivial identity | PJ.TrancheCPrime.ContextTransport.StaticRole.presentation_change_is_load_bearing_noncommutation |
generic identity transport is refuted |
| StaticRole wrong wiring | StaticRole.Countermodels.UptakeHostiles.same_r2_and_evaluator_presentations_disagree_on_r3 |
presentation wiring is load-bearing |
| Continuity same-name without admission | Continuity.Admission.no_name_without_admission and the foreign-packet hostiles |
name/identity equality does not mint admission standing |
| Execution attempt without commit | PJ.Instances.ExecutionCustody.may_attempt_not_entitled_to_commit_without_local_preconditions |
attempted permission does not mint commit entitlement |
| GT projection without runtime correspondence | PJ.Instances.GovernedTransport.MissingPositiveLiftAdapter.native_missing_lift_remains_not_entitled |
projected target evidence does not supply the absent lift |
D-prime additionally reproduces the positive collapse controls: uniformly inhabited receipt fibers, erased subject/context indices, and a consumer that ignores receipt identity all admit minting. Thus anti-minting is exact and adapter-local, not a generic institution.
The public documentation and metadata were searched for affirmative claims of a universal calculus, common judgment algebra, generic composition/frontier, general ownership theory, Planet, Archipelago, complete machine-judgment theory, JCP implementation, or operational AG/NQ realization. Matches in the v15 records are explicit negations or preserved historical classification alternatives, not public claims.
One stale README section still described Governed Transport custody as pending. This commit replaces it with the exact operator-ratified integration status and Atlas scope fence. No other correction is required.
There is one authoritative Continuity implementation, historical Someone
provenance remains visible, every public Lean path carries one exact custody
class and target owner, campaign records retain immutable pins, and generated
indexes retain all four negative classifications.
V15 provides faithful cross-calculus mappings among GT, Execution Custody, and Continuity Admission, preserving exact judgment indices, local countermodels, and receipt-bound entitlement. 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.