Zero Paradox Version Registry
Update this file first on any version bump. README.md Framework table and GUIDE.md Reading Paths are verified against this register.
| Document | Formal Version | Filename | Companion Version | Comp AR | Notes |
|---|---|---|---|---|---|
| ZP-A Lattice Algebra | v1.21 | ZP-A_Lattice_Algebra.pdf | v1.11 | N/— | v1.21: OQ-A1b minimal-element note corrected (bedrock, cross-document attribution) — struck “a metric result, established by ZP-B’s 2-adic structure”; ZP-B proves no minimality and cannot (2-adic norms accumulate at 0; its eps0=2ᵏ is a chosen cutoff). Axiom-mistaken-for-result: the preceding paragraph already attributes this to AX-B1, so the two contradicted each other. Now rests on AX-B1 (per CLAIMS.md); ZP-B’s actual results at 0 stated (clopen T3, irreversible C3); dense counterexample points at ZP-F (axb1_fails_in_ordered_field).v1.20: R-AFA false premise corrected (bedrock, same class as ZP-E v3.24) — struck BOTH squeeze legs (well-founded⟹external-interpreter; bounded ∈-rank vs unbounded surprisal — orthogonal, ∅ has rank 0 yet v₂(0)=∞); Foundation-incompatibility now rests on ⊥={⊥} self-membership (no_quine_atom); R3/L-INF demoted to corroboration; forcing machine-checked (QuineHost); falsifier narrowed; now consistent with the corrected ZP-E R-AFA.v1.19: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.17: C8 dual-date — subtitle templated via version_line (First released / This version); hardcoded month removed. v1.16: FMC uniformity (Step 4b) — residual AFA-necessity assertions softened to “argued” (metatheoretic declaration, R-AFA cross-framework note, CC-2 validation-table cell); comp v1.10 same. v1.15: FMC precision (sweep Step 4, against fmc.md) — CC-2 box “structurally required”/”ruled out”/”incompatible” softened to “argued”; named falsifier added; status line marked argued, not a derivation. v1.14: CC-2 label → Forced Metatheoretic Commitment — formal:93e545f3 comp:7f40ab94 |
| ZP-B p-Adic Topology | v1.14 | ZP-B_pAdic_Topology.pdf | v1.12 | N/— | v1.14: D5 + R1 self-contradiction resolved (Tim, 2026-07-29) - eps0 is UNITLESS. The box asserted it was “a dimensionful quantity” (the v1.12 wording below), then disclaimed any physical-unit magnitude claim, then labelled the status “universe-contingent parameter” - three sentences about three different objects. eps0 is a POSITION (Ordinal.epsilon 0, Veblen (1,0)) and a position carries no units. What is contingent is D5’s real-valued threshold 2^k on the CHOSEN exponent k - a normalisation, not a measurement. R1’s “determined by physical constants” corrected in the same change; Valuation/Padic.lean likewise. This retracts the v1.12 dimensionful/Buckingham-pi framing recorded below.v1.13: D5 exponent/valuation conflation corrected - “eps0 = 2^k where k is the maximum valuation accessible” contradicts the document’s own ball convention B(0, 2^-n), since a MAXIMUM valuation gives a MINIMUM scale: k = -v. No semantic change; Valuation/Padic.lean carried the same conflation and is corrected with it.v1.12: D5 Planck-scale reference struck - the last live site in the corpus (Foreword cut it v1.8, both companions v1.3, ZP-B never did). An adversary review called it a crank signal in 2026-05. Replaced with the structural reason the value is contingent: eps0 is DIMENSIONFUL, so its value depends on a unit choice and cannot be instantiation-independent.comp v1.12: PRECISION FIX (release-prep) — grounded the companion’s clopen/distance prose in the formal ZP-B claims (C3 no-continuous-path, T5 total disconnectedness): zero is a LIMIT of nonzero states (not isolated; the v1.4/v1.7 correction), v₂(0) is an infinite VALUATION not a distance (2-adic distances stay finite), placing zero in a clopen class distinct from every nonzero state; the only crossing is the discrete-jump Snap. General-reader register kept.C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.10: rendered self-version tags removed from C2/C3 corollary titles + “null state” → ⊥ in AX-B1 note (C1 sweep) — formal:14cbf9ae comp:1274729d |
| ZP-F The Counterexamples | v1.6 | ZP-F_The_Counterexamples.pdf | v1.14 | N/— | v1.6: FORCING OVERCLAIM RETRACTED. The document described the snap as a forced transition with no occurrence hedge anywhere. T-SNAP fixes the transition’s SHAPE; tsnap_holds_but_nothing_moves proves it holds in a model where nothing moves, so occurrence is a framework commitment. Prose only.comp v1.14: FORCING OVERCLAIM RETRACTED (bedrock, cross-document attribution). The key-result table asserted “The snap is a theorem - the valuation gap forces it”; Valuation/Padic.lean calls that ground FALSE by name in the same push - the valuation gap yields no first step, and no metric result could. The first step is AX-B1, a commitment. Section IV heading and its body sentence likewise moved from “forces the snap” to “makes the snap possible” / “becomes available”.C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.4: vocab fix — “null state” → “⊥” in preamble; palette rebuild — formal:ce397179 comp:d6bdb1f7 |
| ZP-C Information Theory | v1.21 | ZP-C_Information_Theory.pdf | v2.7 | N/— | v1.21: self-containment note names the ZP-A cross-layer dependency (T-BUF invokes ZP-A D2, the state-transition definition; Lean Order/Lattice.lean).v1.20: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.18: rendered self-version refs removed — P₀ note (“Version 1.4 updates this”) + Open Items row (C1 sweep) — formal:39391a34 comp:fb2cd7c4 |
| ZP-D State Layer | v1.15 | ZP-D_State_Layer.pdf | v1.13 | N/— | v1.15 / comp v1.13: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).v1.14: R-PA prior-art note — T is the standard p-adic ball-indicator ONB (van der Put basis) / Kozyrev p-adic wavelet basis (Kozyrev 2002), with p-adic-QM context; paired with the CLAIMS Convergence row. C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.12: rendered self-version refs removed — DP-1 title tag + T2 “R3 (v1.6)” (C1 sweep) — formal:f644e376 comp:db8ed80e |
| ZP-E Bridge Document | v3.25 | ZP-E_Bridge_Document.pdf | v1.12 | N/— | v3.25 / comp v1.12: FORCING OVERCLAIM RETRACTED. The document asserted that T-SNAP establishes the snap OCCURS; it does not. T-SNAP fixes the transition’s shape, and Order/Snap.lean’s NO-GO gauge tsnap_holds_but_nothing_moves proves T-SNAP holds in a model where nothing moves. Occurrence is a framework commitment. Prose only. Four ZP-E sites (the branching-tree implication, the OQ-E1 row, and two claim-table validity grounds); OQ-E1 is now “closed given the occurrence commitment”, matching CLAIMS.md and the DA-1 row’s existing “closed given DP-2” form. The companion described “the forced first transition in any join-semilattice”, which the gauge itself refutes (its MachinePhase IS a join-semilattice in which nothing moves); its § on DA-1 also reworded to drop a banned vocabulary term that had been blocking its rebuild.v3.24: R-AFA false premise corrected (bedrock) — struck the invalid well-founded⟹finite-tree step (ω is well-founded and infinite); Foundation-incompatibility now rests on the self-membership of ⊥ = {⊥} (no_quine_atom, choice-free); forcing + realizability stated machine-checked (QuineHost — quineHost_not_wellFounded, oneAtom_not_wellFounded, afaStructure_isQuineHost); CC-2 = Forced Metatheoretic Commitment (not Conditional Claim); named falsifier narrowed to the requirements-choice; CC-1 “modelling commitment” → “derived via ZP-J”, DA-3 link hedged to conjecture, endnote de-changelogged.v3.23: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v3.21: FMC precision (sweep Step 4, against fmc.md) — R-AFA “the metatheoretic necessity of AFA is derived” → “argued, not proved (a metatheoretic squeeze, not a derivation)” + named falsifier added; CC-2 status lines split the proved structural fixed point (T-EXEC, axiom-free) from the argued set-membership reading; “establish that Foundation is incompatible” → “make the case that” — formal:9576e27a comp:dffeb905 |
| ZP-G Category Theory | v1.15 | ZP-G_Category_Theory.pdf | v1.9 | N/— | v1.15: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).v1.14: R-AX named AX-G2 as the standard strict-initial-object property (Carboni-Lack-Walters 1993) + the AX-G1+AX-G2 = non-trivial-strict-initial note; prior-art positioning paired with the CLAIMS Convergence section. C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.12: rendered self-version refs removed — 24 status/provenance tags + “Version 1.0…1.1” narratives + Supersedes (C1 sweep; cross-doc ZP-H v1.0 citations kept) — formal:2af3526b comp:e9014e47 |
| ZP-H Categorical Bridge | v1.18 | ZP-H_Categorical_Bridge.pdf | v1.14 | N/— | v1.18: FORCING OVERCLAIM RETRACTED (Remark R-FORCING). F_B was said to “force an irreversible jump at 0” - Valuation/Padic.lean retracts exactly that ground: the 2-adic topology proves irreversibility and a clopen gap, never a first step. The closing “structurally forced across all four” now scopes to the SHAPE; occurrence stays a framework commitment.C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.16: rendered self-version removed — endnote + R-FORCING tag (C1 sweep; 21 cross-doc citations kept per scope) — formal:fe2b0c34 comp:b81238d3 |
| ZP-H Native Categories Addendum | v1.2 | ZP-H_Native_Categories_Addendum.pdf | N/A | N/— | C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.2: rendered Lean-file citations synced to post-reorg basenames (ZPH_* -> *, ZPH_MC1 -> MC1Bridge).v1.0: Initial release — snap floor realized in native Mathlib categories: fB_functor → TopCat (⊥ = inverse limit ⋂ B(0,2⁻ⁿ) = {0}), fD_functor → ModuleCat ℂ (⊥ = StateSpace 0 initial; isometric embeddings), fC_functor → KleisliCat PMF (⊥ = Fin 0 initial; fC_no_return = AX-G2 as theorem); mc1_correspondence capstone. Correspondence half of MC-1 formal; identity half retired as ill-typed (members provably distinct). Lean: ZPH_TopFunctor/ZPH_HilbFunctor/ZPH_InfoFunctor/ZPH_MC1.lean; [propext, Classical.choice, Quot.sound] — formal:00d1d40a |
| ZP-I Inside Zero | v1.15 | ZP-I_Inside_Zero.pdf | v1.24 | N/— | comp v1.24: FORCING OVERCLAIM RETRACTED (companion sync with ZP-I v1.15) - “T-SNAP (bottom -> eps0, necessarily)” asserted occurrence; an occurrence fence was added and its scope corrected to cover the whole document.v1.15: FORCING OVERCLAIM RETRACTED. The document asserted that T-SNAP establishes the snap OCCURS; it does not. T-SNAP fixes the transition’s shape, and Order/Snap.lean’s NO-GO gauge tsnap_holds_but_nothing_moves proves T-SNAP holds in a model where nothing moves. Occurrence is a framework commitment. Prose only. Three sites, all using the word “necessarily” rather than “forced” - which is why two earlier greps did not reach them.v1.14: PURITY CORRECTION (release-prep) — “axiom-free” was wrong for the p-adic convergence spine; t_iz_cauchy / t_iz_valuation_unbounded / t_iz_c3_compatible / t_iz_complete / t_iz_h_bound_from_depth_chain carry Classical.choice (inherited from Mathlib p-adic analysis, not a framework commitment); only Step 6 (t_iz_limit_is_new_null) + t_snap_derived are axiom-free, c_t_iz_null_balance is [propext]; ~15 rendered claims corrected. Verified vs #print axioms.v1.13 / comp v1.23: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.11: rendered self-version removed — register section headers + T-IZ status cells + endnote (C1 sweep) — formal:42af5769 comp:a4d269d9 |
| ZP-J Self-Reference | v2.5 | ZP-J_Self_Reference.pdf | v1.29 | N/— | comp v1.29: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v2.5: rendered Lean citations synced to post-reorg files/namespaces the v2.4 pass missed (ZPJ.lean -> SetTheoryAFA.lean; ZeroParadox.ZPJ.* -> ZeroParadox.* namespace flattened; ZPE.da2_bottom_characterization -> bare, now in Snap.lean).v2.4: rendered Lean-file citations synced to post-reorg basenames (ZPJ_AczelConn.lean -> AczelConn.lean, etc.).v2.2: rendered self-version refs removed (C1 sweep); null glyphs fixed. comp v1.26: FMC precision (sweep Step 4) — Key Results box + T-EXEC body line split the proved structural fixed point (axiom-free) from the argued set-membership reading. comp v1.25: ScaleBridge wired into maintained build → §6 “future work” bridge retired (2-adic argument now formalized), §7 common-ancestor (ValBridge) framing added, §8 adds ℤ₂ as 3rd concrete model (flagged Classical.choice-carrying vs axiom-free T-EXEC). comp v1.24: APG directed-graph diagram (self-loop), arithmetic analogy scoped, depth rephrased to intrinsic descent, self-loop redrawn as dashed curve (Dan 2026-06-15) — formal:146e11b1 comp:578c9d76 |
| ZP-J AFA Addendum | v1.7 | ZP-J_AFA_Addendum.pdf | N/A | N/— | v1.7: Lean Source Files box lists SetTheoryAFA.lean (AFAStructure typeclass home); “seven”→”eight” source files; stripped “as of May 2026” dated qualifier from endnote.v1.6: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.5: rendered Lean-file citations synced to post-reorg basenames (ZPJ_* -> *).v1.3: rendered self-version ref removed from endnote (C1 sweep); fixed scaleᵏ null glyph — formal:e7ca7b90 |
| ZP-J Wheel Addendum | v1.3 | ZP-J_Wheel_Addendum.pdf | v1.3 | N/— | C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.3: rendered Lean-file citations synced to post-reorg basenames (ZPJ_Wheel/WheelFrac -> Wheel/WheelFrac).v1.1: WheelFrac.* citations → ZPJ_WheelFrac.* (Lean namespace standardization); comp v1.1 same. v1.0: Initial release — wheel of fractions ⊙_S A = (A×A)/≡_S is a Wheel (Carlström Def 1.1, 14 fields), choice-free [propext, Quot.sound]; inf_ne_bot porthole (∞≠⊥ given 0∉S). Lean: ZPJ_WheelFrac.lean; fix() guard added (PDF build standards). comp v1.0: ZP-J_Wheel_Illustrated_Companion.pdf — plain-language (division-by-zero made total; ∞=/0, ⊥=0·/0; wheel-vs-meadow diagram; instWheel + inf_ne_bot; porthole connection) — formal:ed028de2 comp:0ba1f949 |
| ZP-J Keystone Addendum | v1.5 | ZP-J_Keystone_Addendum.pdf | N/A | N/— | v1.5: THE v1.4 FIX WAS PARTIAL, WHICH MADE IT WORSE. v1.4 corrected the two sites carrying the forbidden PHRASES and missed a third stating the same claim in other words (“The one-object identification remains the MC-1 commitment”), leaving the document saying the identity was retired on page 1 and live on page 2 - before v1.4 it was uniformly stale, i.e. self-consistent. A partial fix to a self-consistent error manufactures a self-contradiction. Both gates returned FAIL-BEDROCK. A FOURTH site then surfaced, flagged by neither gate, found only by sweeping the RENDERED text for the CLAIM (any sentence pairing an identity notion with a live-status verb) rather than for phrases: section III called MC-1 an “existing identification” and its “bottom/epsilon-zero identification” wording could be read as equating the endpoints, which epsilon0ne_bot forbids; now a role assignment with the distinctness named. Endnote Lean sources upgraded to full repo paths.v1.4: MC-1 FRAMING brought to the ratified form (KEY-1, a release blocker). THREE rendered sites (v1.4 fixed two, v1.5 the third) called the cross-category identity a live “modeling commitment” and said it was “offered” - that identity was RETIRED AS ILL-TYPED (an equation across distinct categories is not a well-formed proposition), and CLAIMS.md already said so, so the PDF disagreed with the ledger. Now: family membership proved per domain, criteria a design principle, identity retired, members provably distinct. Also KEY-2: Cor 8.2 lists FIVE equivalent conditions (the docstring had said “three-way”); the category/functor split restated unambiguously (smooth-monos and subobject-classifier are the CATEGORY’s; preserving inverse images and the pre-fixed point are the ENDOFUNCTOR’s; routes not exhaustive); prior-state prose narrating an unshipped draft removed from the docstring, which ships publicly via scripts/. R2-4 (Taylor cited page-precisely with no year or venue) NOT fixed - the on-disk copy carries neither and inventing them is worse than the gap.v1.3: CITATION SCOPE - section III called the biconditional “the General Recursion Theorem”; AMM Thm 7.2 p.27 is the FORWARD direction only, their section 8 is its converse. That converse asks the ENDOFUNCTOR to preserve inverse images plus one of SEVERAL routes (Thm 8.1 smooth-monos+pre-fixed-point / Thm 8.6 subobject classifier / Thm 8.12 vector spaces) - the first two conditions are the CATEGORY’s, not the functor’s, and they are not exhaustive; Cor 8.2 gives the equivalence under Thm 8.1’s assumptions. Taylor’s necessity scoped as he scopes it, IN A TOPOS (Prop 111 p.6, stated not proved), forward half at Thm 36 p.15; the “cannot recurse through the bottom” reading marked as this framework’s gloss. Next-time operator no longer listed as missing (built at ZeroParadox/Category/NextTimeCategorical.lean); remaining Mathlib absences dated, not asserted.v1.2: rendered Lean-file citations synced to post-reorg basenames (ZPJ* -> *).v1.1: honest-scope precision — the single-carrier “snap is one crossing” carries no NEW commitment; it rests on the framework’s existing ⊥/ε₀ identification (MC-1 / OQ-E2), endpoints proved (floor non-wf via real ⊥, axiom-free). v1.0: Initial release — thin addendum recording two machine-checked keystone probes. (1) Lawvere face-split (ZPJ_Lawvere.lean): in Set no face is a Lawvere instance (Cantor — nontrivial_lattice_no_witness, q2_no_witness), the computability face genuine (computability_face_fixedPoint, wraps Mathlib recursion theorem); fixedPoint_of_witness / no_witness_of_fixedPointFree axiom-free. (2) Well-foundedness boundary (ZPJ_Boundary.lean, ZPJ_BoundaryBridge.lean): the snap as a ν→μ crossing — relation level (floor_not_wellFounded axiom-free; snap_crossing) + QPF bridge (snap_boundary_two_registers), best-effort; full Taylor coalgebraic (next-operator / Pataraia / General Recursion Theorem) open, cited to Taylor/AMM. Honest fences throughout (probe; no-new-commitment; open Rung-C) — formal:67f1d971 |
| ZP-K Computational Grounding | v1.14 | ZP-K_Computational_Grounding.pdf | v1.17 | N/— | v1.14 / comp v1.17: “Rogers’ fixed-point theorem” corrected from “Roger’s” (Hartley Rogers Jr.). ZP-L made this exact correction at its v1.4 and it was never swept to the rest of the corpus; Mathlib carries the same typo upstream at Computability/PartrecCode.lean:36,1001. Prose only, no claim changed.v1.13: BEDROCK - the class-field-as-theorem root cause propagated to six sites. botCode and botCode_is_quine are now named as a CLASS FIELD carrying a periodicity condition that constant codes also satisfy, not as a witness that “botCode IS its own program”; the preamble no longer says Kleene’s theorem “provides the formal witness”; Section III and the verification table said “four-way equivalence” where t_comp proves THREE. R-K.0 gains the type-level statement of the gap: (1)-(3) are properties of an element of L, (4) of a Code, with no function between them anywhere in the development.v1.12: witness audit - bot_self_mem_from_kleene is a RESTATEMENT of the inherited AFAStructure field, not “the Kleene side implies the AFA side”; the two conditions are class FIELDS and their sameness is the framework’s reading, the motivation for the class rather than something derived in it.v1.11: DA-1 Path 3 RECLASSIFIED (Tim, 2026-07-27) from CLOSED / IN SCOPE to FOUNDATIONAL COMMITMENT, matching Path 2 and CLAIMS.md. Its witness botCode_is_quine is a class field assumed at instantiation, not a second independent proof.v1.10: T-COMP overclaim corrected (bedrock) - preamble no longer says the four roles “are shown to be the same structural object” (three PROVED to coincide; the computational role is a KleeneStructure typeclass field, as R-K.0 already stated); footer chained cross-type identity replaced; “DA-1 closed” narrowed to “DA-1 structural half”. Companion v1.13 same class.v1.9 / comp v1.12: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.7: version changelog removed from preamble; palette rebuild. comp v1.10: four_way_diagram — removed the redundant internal caption String that overlapped the “Computation (Kleene)” box (Diagram Rule 4). comp v1.9: FMC precision (sweep Step 4) — DA-1 Path 1 splits the axiom-free structural fixed point from the literal ⊥={⊥} (ZF+AFA setting) — formal:1b9ec06e comp:524955ee |
| ZP-L Incomputability Convergence | v1.6 | ZP-L_Incomputability_Convergence.pdf | v1.6 | N/— | v1.6: FORCING OVERCLAIM RETRACTED. The document called the snap “the forced transition” with no occurrence hedge anywhere. T-SNAP fixes the transition’s SHAPE; tsnap_holds_but_nothing_moves proves it holds in a model where nothing moves, so occurrence is a framework commitment. Prose only.v1.5: axiom-footprint list label corrected - t_comp is a three-way equivalence, not four (the computational face is an assumption, not a clause). Footprint figures unchanged.v1.4: “Rogers’ fixed-point theorem” corrected from “Roger’s” (Hartley Rogers) — Section II heading + prose.v1.3 / comp v1.6: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.1: rendered version changelog removed + 3 null glyphs fixed (subscript-letter entities ₙ/ₒ → markup) (C1 sweep); comp v1.4: strip footer version — formal:04df89fb comp:1b075124 |
| ZP-M Kleene-Ordinal Bridge | v1.3 | ZP-M_Kleene_Ordinal_Bridge.pdf | v1.5 | N/— | v1.3 / comp v1.5: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.1: rendered version changelog removed from title note + endnote (C1 sweep); v1.0: snapEmbed type bridge, hfp gap closed, zpm_triangle, R-M.1; comp v1.3: rendered self-version removed from Key Results header (C1) — formal:b510ab50 comp:0af8ce63 |
| ZP-N The Constructive Snap | v2.0 | ZP-N_The_Constructive_Snap.pdf | N/A | N/— | v2.0 (2026-07-20): Major revision — corrects v1.0’s mechanism and adds the construction it was missing. The ascent is constructive (unchanged, still the layer’s genuine content): exp_lt_term, omegaPow_no_fixedpoint, tower_strictMono, all [propext] only. NEW: (a) the classical dependency is located and shown load-bearing — comparability of arbitrary well-orders implies excluded middle (em_of_wellOrder_comparable, [propext, Quot.sound]); the taboo is Kraus/Nordvall Forsberg/Xu arXiv:2104.02549 Thm 38(d), cited not claimed, and is a PAPER proof (no machine-checked version located). (b) the footprint instrument is shown uninformative for ε₀ results — choice sits in the Ordinal.partialOrder INSTANCE TERM, so a ≤ a carries it and a = a does not (order_footprint_le / order_footprint_eq). (c) a carrier sized to the job — E0Note = WithTop ONote, crossing into Ordinal via one named map e0Repr; carrier choice-free, crossing carries Classical.choice at every decl; construction credited to Castéran (hydra-battles ON_plus/ON_correct carry his name alone; the library is his and Contejean’s), ON_correct NOT claimed - only the first of its three fields is established (e0Repr_not_injective), top fixed point STIPULATED. Whether ZP-L’s ε₀ results are eliminable remains UNCLASSIFIED. Minimality (ε₀ the LEAST fixed point) open. Lean: ConstructiveOrdinals.lean, SnapNucleusConstructive.lean, OrdinalChoiceEssential.lean, PricedInterface.lean — formal:5011bb68 |
| ZP-P The Fixed-Point Fork | v1.23 | ZP-P_The_Fixed_Point_Fork.pdf | N/A | N/— | v1.23: two defects in ONE rendered p.4 sentence, both from the v1.22 fix. (1) The restored carrier phrase went in at the wrong POSITION here while all eight Lean sites got the clean order, so the publication site read “with no axioms over that M-type” — nearest-head parsing gives something meaningless. (2) The dangling pronoun was REPORTED as fixed in v1.22 and was not touched: “The M-type FORMER and constructors are axiom-free, ITS DESTRUCTOR …”. Both corrected; the checkable sites and the published one now read identically. Worth recording the shape: the sites a gate can grep got the good wording and the one that renders got the degraded one.v1.22: the v1.21 CLASS sweep missed a member, and said it had not. (1) It claimed to have reached every site; ChoicePurityInvariant.lean wrote the phrase as is **axiom-free** — markdown bold INSIDE the phrase — so the literal pattern did not match, in a file that same commit edited twice. Fixed, and v1.21’s claim corrected to “the live sites” because it was false as written. GREP LOOSELY: markup inside a phrase defeats a literal pattern. (2) The sweep also DELETED a load-bearing carrier phrase — strict_cofix_nonempty is over the M-TYPE, not over Cofix, so “proves the same inhabitation” took cofix_nonempty as its nearest antecedent and read as contradicting its own preceding clause; “over the M-type” restored everywhere including the rendered p.4 box. (3) Proposition 9 is in the paper’s section 2, which one sentence still contradicted 25 lines above the fix. All three caught by gate round 1.v1.21: swept the CLASS the v1.20 fix left behind, plus the widow. (1) The discredited WARRANT “PFunctor.M is axiom-free” survived at 13 live sites after v1.20 removed the false CONCLUSION it supported — one Lean file carried the precise account and the loose one 55 lines apart. It is true of the TYPE FORMER and silent about the ELIMINATORS (M.children / M.dest carry the axiom), so the live sites now state former / constructors / destructor separately. (2) The Theorem Summary table orphaned cofix_nonempty alone on p.6 under a repeated header, reported by three consecutive gate rounds and surviving three rebuilds; it now starts on its own page, since nudging spacing only changes which row is orphaned.v1.20: BEDROCK — the v1.19 sweep fixed the two-page contradiction and swept to a FALSE statement. It said the choice is “not from the M-type underneath”, warranted by “PFunctor.M is axiom-free”. That is a witness-vs-statement defect: PFunctor.M is the TYPE FORMER and its purity says nothing about its eliminators. Measured: PFunctor.M / .mk / .corec are axiom-free, but M.children and M.dest carry [propext, Classical.choice, Quot.sound], and QPF.Cofix inherits from them via Mcongr/IsPrecongr — so the choice DOES come from the M-type, from its destructor. The true account is stronger and is now what the remark box says: strict_cofix_nonempty is axiom-free because it only BUILDS (M.corec) and never DESTRUCTS. Caught by the gate, which measured the claim rather than reading it.v1.19: the v1.18 fix swept ONE of the sentence’s sites. Two more rendered — p.4’s result box and p.6’s Axiom Purity box both still attributed the choice to “the M-type / corecursion machinery”, so the published document said “not from the M-type underneath” on p.4 and “from the M-type …” on p.6, contradicting itself across two pages. Both now say QPF corecursion / quotient layer, which is what the measurement supports (QPF.Cofix carries the axiom in the type; PFunctor.M is axiom-free). Caught by gate round 2, which correctly ruled it ordinary: QPF.Cofix IS the quotient of PFunctor.M, so the loose name was imprecise rather than false and no conclusion rested on it.v1.18: the v1.17 clarification was PREPENDED and the original attribution left standing, so the remark box read “inherited from Mathlib’s M-TYPE MACHINERY … not the M-TYPE underneath” — one sentence contradicting itself. Same prepended-hedge shape as v1.10, and the seventh time this document has produced it. Rewritten once, attribution first: the choice comes from the QPF quotient layer, QPF.Cofix carries it in the type, PFunctor.M is axiom-free. Caught by gate round 1 on the modal-claim sweep.v1.17: MEASURED, replacing an inference. Two rendered sites called the nu-side Classical.choice “a library artifact, not a necessity” and “not forced by the mathematics”. True in spirit, unmeasured as stated. Measured 2026-08-03: QPF.Cofix carries Classical.choice IN THE TYPE, so no proof of any Cofix-mentioning statement is choice-free — it is not removable by rewriting. What makes it an artifact is the pair: PFunctor.M is axiom-free and strict_cofix_nonempty proves the same nu-inhabitation over it with NO axioms, so the choice belongs to the QPF quotient layer and escaping it means changing the carrier. Found by the new modal-claim sweep (.claude-local/check_modal.py).v1.16: THE SENTENCE IS DELETED (Tim). Two remark-box bullets characterised the choice modality of Veltri’s finite-powerset presentations. That material was wrong in SIX consecutive versions (v1.9 a universal, v1.10 a doubling, v1.11 the universal restored, v1.13/v1.14 a false universal, v1.15 a false uniqueness), each fix locally reasonable and each seeding the next. It was never load-bearing here: ZP-P’s claim is that the Classical.choice in cofix_nonempty is a Mathlib artifact for a POLYNOMIAL functor, which bullet 1 states and ACS supports. The finite-powerset material is now one sentence saying it is a different case, out of scope, and recorded in ZeroParadox/Settheory/Coalgebra.lean, where the gates have verified it against the source. Prose that cannot be kept correct across six attempts does not belong in a published PDF when an accurate statement of it already exists in a checkable file.v1.15: BEDROCK — the v1.14 fix replaced a false UNIVERSAL with a false UNIQUENESS. “not all of them use it, and the exception is the one he prefers”: Veltri has TWO choice-free finality results, not one — Theorem 1 (the setoid presentation, final in SetoidRel, proved by anaTree with no classical hypothesis) as well as Theorem 2 (the coinductive type). His stated reason for preferring (ii) over (i) is ergonomic, that it “does not force the user to employ setoids instead of types”, which is exactly what “the exception” erased. FIFTH consecutive version in which this one sentence has been wrong; the quantifier is deleted rather than re-hedged and both theorems named. The truth was STRONGER than the claim, so the fix cost nothing. Also: Propositions 59 and 60 relocated to the paper’s section 8 (Approximating Subtraction, Division and Logarithm Operations) — they are not in the taboo section 7 — and the orphaned “each” given its referent.v1.14: BEDROCK — the v1.13 remark box carried a false universal about Veltri. Bullet 2 said “his finality results are obtained assuming choice principles”, and bullet 3, added by v1.13, named the construction that refutes it: his preferred coinductive type (his Theorem 2) needs neither choice nor LLPO. The v1.13 fix added the counterexample and left the universal it contradicts standing one bullet above — the same half-sweep shape as v1.10’s doubling. Bullet 2 is now scoped to the proofs that do use choice, and its duplicate LLPO-necessity clause removed. Also corrected in the Lean sources: Proposition 60 (iii) is separated from the CONSTRUCTIVE Proposition 59 (iii) by the SCOPE OF MAXIMALITY, not by the gamma <= beta bound, which both carry — v1.13 had asserted the inverse, an error imported verbatim from three round-3 reviewer notes and applied without checking it at the source.v1.13: gate debt cleared in one batch rather than carried as next-touch debt. The “not a necessity result” gloss was unscoped — it covered the LLPO half too, and LLPO is the one thing Veltri DOES prove necessary (p. 22:3 is an impossibility); scoped to the choice half. Also added his choice-free construction (ii) to the remark box: the Lean file carried that counterexample and the PDF did not, which is why the “all of” universal regenerated three times here — the box had no visible instance refuting it.v1.12: the v1.11 fix relocated its error for the THIRD time in one sentence — v1.9 said choice enters “only for” the finite-powerset functor (a universal), v1.10 PREPENDED a hedge and left the clause standing (a doubling), v1.11 removed the doubling and the hedge together and restored the universal as “are all of”, which the same remark box contradicts two paragraphs up where it concedes that Mathlib’s presentation of the POLYNOMIAL functor idPF_Coalgebra carries Classical.choice. The universal is now deleted rather than re-hedged. Also restored LLPO to the Worrell clause: Veltri’s Conclusions and abstract both give construction (iv) as countable choice AND LLPO, and v1.11 had dropped it, leaving this document disagreeing with CLAIMS.md, which was right.v1.11: retrospective gate round on already-published text. The v1.10 hedge was PREPENDED and the original clause left standing, so the remark box read “In the cases the literature pins … where the literature pins each presentation” — one clause doubled; rewritten once. Also retired the “genuinely enters” framing (remark-box heading and body): choice in the pinned finite-powerset presentations is a fact about those constructions, not a necessity, and Veltri’s own preferred coinductive construction needs neither choice nor LLPO.v1.10: the v1.9 abstract fix RELOCATED its error rather than removing it — it made the theorem statement true but added a clause asserting that the framework’s own operators are monotone self-maps of a complete lattice, which the corpus explicitly denies and this document’s Section III calls open. Clause replaced by an explicit non-claim.v1.9: adversary review of the rendered document pre-publication — three substantive fixes: the abstract stated Knaster-Tarski WITHOUT monotonicity (false as written; the swap on the two-element lattice has no fixed point), the Tier-3 roster named the categorical INITIAL object as a contact point where Section II proves that object empty and locates the analog in the FINAL coalgebra, and quine_atom_unique was cited for two things it does not state.v1.8: swept the sibling v1.7 left standing — the next rendered paragraph still said the set-quotient and Worrell presentations REQUIRE choice, the modality v1.7 had just retired one sentence earlier; Veltri’s own wording is “requires the presence of the axiom of choice in the proof of finality”, about his proof rather than a necessity result.v1.7: the LLPO claim given its hypothesis — injectivity of the canonical algebra implies LLPO outright (Veltri Cor. 8, explicitly without countable choice) and is equivalent to it only under countable choice (Thm 9); the v1.6 changelog’s own modality brought in line with the corrected prose.v1.6: CORRECTED a misattribution in rendered prose — choice-free constructibility of the final coalgebra FOR A POLYNOMIAL FUNCTOR was credited to Veltri (FSCD 2021) in the Lean-witness table and co-credited in the remark box; that is the wrong direction (his subject is the finite-powerset functor, which is NOT polynomial, and his results there are obtained ASSUMING choice principles rather than shown to need them — he hands the polynomial case to Ahrens-Capriotti-Spadotti himself). Now attributed to ACS (TLCA 2015), with Veltri explicitly marked as contrast; his LLPO claim, which IS his and IS about finite-powerset, unchanged.v1.5: rendered Lean citations synced to post-reorg files/namespaces (SSOT-driven).v1.4: rendered Lean-file citations synced to post-reorg basenames (ZPP_* -> *).v1.3: re-aimed the categorical-instance choice note per Veltri (FSCD 2021) literature review — the ν-side Classical.choice is a Mathlib M-type artifact, not a necessity (polynomial-functor final coalgebras are choice-free); choice genuinely enters only for the non-polynomial finite-powerset functor (full AC for the set-quotient; countable choice + LLPO for Worrell’s limit); added “where choice genuinely enters” remark + Veltri/Ahrens citations (R1). C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.1: Added categorical-parent instance as Lean witness (ZPP_Coalgebra.lean: fix_isEmpty μ-empty choice-free, cofix_nonempty ν-inhabited Classical.choice, categorical_fork_strict); set theory/computation referenced (ZP-J/ZP-K) not re-framed. v1.0: synthesis layer — abstract fork schema (lfp/gfp collapses iff unique fixed point) choice-free in Lean: fork_le, collapse_of_unique, unique_of_collapse, fork_collapse_iff [propext, Quot.sound]; number-system instance via Ostrowski: completions_exhaustive, real_not_equiv_padic [propext, Classical.choice, Quot.sound]. Generalizes ZFC+Foundation/AFA orthogonal-contact-point claim; three tiers (schema/instances/unification), hard fence (cross-instance identity = type boundary) + soft fence (not every fork is μ/ν). Lean: ZPP.lean, ZPP_Ostrowski.lean, ZPP_Coalgebra.lean — formal:a83dbbf3 |
| ZP-R Cross-Category Fixed Point | v1.0 | ZP-R_Cross_Category_Fixed_Point.pdf | N/A | N/— | v1.0: Initial release. Synthesis / placement layer — locates and realizes the framework’s self-application fixed point ⊥ as a Lawvere fixed point across three faces: refuted in Set (Cantor; reflexive_object_refuted, not_monotone_not), obstruction-free but not a reflexive object in the monotone/domain regime (monotone_regime_derives_pinned; Scott D∞ unbuilt), realized in the computability face (eval_point_surjective, computable_no_fixedpointfree, selfref_fixedpoint_exists_computable — the crossing). R1 fork (fork_collapse_iff via instance_pinnable_iff_fork_collapse); R2a/b existence-as-selfApp + uniqueness-extra (lawvere_fixedpoint_selfApp, selfApp_pinnable, existence_without_uniqueness); R4 μ/ν = Lawvere regimes (mu_nu_branch_exclusion). Scope: existence-as-Lawvere (computability face) vs uniqueness + location (fork/AFA face: t_exec/t_exec_iff, quine_atom_unique, unique_fp) each proved but face-local and non-composable (F1/F2) — the computability face is non-unique (infinite_quine_family). Global identification held as a fenced conjecture. Choice-free spine, choice-carrying computability realization. Lean: RequirementsGap/MetaFork/LawvereBridge/SetTheoryAFA/SelfApp/ComputableCrossing/Kleene — formal:3bcf9350 |
| ZP-R Diagonal Family Addendum | v1.0 | ZP-R_Diagonal_Family_Addendum.pdf | N/A | N/— | v1.0: Initial release. Addendum to ZP-R — the complete diagonal-family roster tied to ⊥, organized by the μ/ν fork. Supersedes the private ZP-W “Zero as a Wall” draft. Engine: negation_no_fixedpoint, lawvere_fixedpoint (Wall.lean; choice-free). Wall faces μ (self-reference cannot close): Cantor (cantor_via_engine), Russell (russell_via_engine), Turing (no_self_decider), the wall wf_no_selfloop — all Wall.lean choice-free; Tarski (tarski_no_internal_truth, Tarski.lean), Curry (curry_paradox/curry_no_bottom, Curry.lean). Floor faces ν (self-reference closes): Quine atom (t_exec/t_exec_iff, SetTheoryAFA.lean), Kleene quine (computability_face_fixedPoint, Lawvere.lean; choice-carrying), Löb + Gödel 2nd (loeb, godel_two, Loeb.lean; choice-free), Rice exists-but-undecidable (rice_face_has_bottom, quine_exists_yet_rice, Rice.lean; choice-carrying). Gödel 1st between the columns (via lawvere_fixedpoint). Unification = Lawvere 1969 / Yanofsky 2003 (cited); contribution = axiom-free core formalization (computability faces choice-carrying) + tie to ⊥ (placement, not new theorem); cross-face identity a type boundary (ZP-P hard fence / ZP-R F2) — formal:19000586 |
| ZP-Q The Frame-Change | v1.7 | ZP-Q_The_Frame_Change.pdf | N/A | N/— | v1.7: VOCABULARY DECISION, recorded rather than deferred. “instance” was doing two jobs - the technical instance-of-a-theorem relation, and ZP-P’s inherited tier-2 word for a per-domain realization - so after v1.6 answered the universal question in the negative, page 1’s title-block note and page 7’s endnote gave opposite answers about the same two objects purely through that collision. “instance” is now reserved for the instance-of-a-theorem relation; a per-domain realization is a “realization” or a “face”. Five rendered sites; no claim changed. The Lawvere-instance uses in Section III are the technical sense and stay.v1.6: the v1.5 fix was UNSWEPT (adversary round 5). v1.5 corrected Section I to say NONE of the min=max facts is an instance of fork_collapse_iff and left Section III and the endnote byte-identical to v1.1, where Section III answered its own headline question - “one theorem all the instances are cases of?” - in the AFFIRMATIVE for catseam_is_frameflip, the object Section I rules out by name, and the endnote called it an “instance” outright: one PDF asserting and denying the same proposition eight pages apart. Section III now answers in the negative and keeps the true half (the theorem is universal over complete lattices; the faces fail its hypotheses); the endnote says “face”. The denial framing (“they were never the same map”, “the snap is a separate object”) is replaced by the conjectural form per the POV KIND/STATUS convention - the identification is held OPEN, not settled either way.v1.5: the v1.4 fix was half-applied - the rendered text still called selfApp_bot_is_both_extremal and the categorical seam ‘genuine instances’ of fork_collapse_iff. None of the framework’s min=max facts is an instance (it needs a complete lattice and a monotone map); they share a shape, which across distinct structures is a type boundary.v1.4: struck the eps0 half of the same instance claim.v1.3: rendered SUBTITLE still asserted the identification v1.2 struck.v1.2: BEDROCK framing - the layer identified the SNAP with the frame-change; the Lean does not. The frame-change is the POLE EXCHANGE (bottom read as both 0 and infinity); the snap is one covering step off the zero face (AX-B1, a commitment). The snap-as-instance reading remains this layer’s conjecture.v1.1: frame-change prose precision (tower encodings converge to ⊥ / diverge to ∞; ε₀ never “realised as ⊥/the ceiling”, ε₀ ≠ ⊥; theorems unchanged). v1.0: Initial release. Synthesis layer, ZP-P sequel — ⊥→ε₀ as a change of point of view. §I frame-flip schema (fork_is_frameflip, ForkFrameChange.lean; choice-free [propext, Quot.sound]); §II per-domain instances (valuation/Riemann sphere: snap_is_frameflip / RiemannSphere.lean; category: catseam_is_frameflip; set-theory/computability/Hilbert/information referenced; reals NO-GO); §III universal + walls (order-theoretic universal holds; the categorical Lawvere universal meets a proven wall, Cantor/Lawvere.lean; cross-domain identity a type boundary). Three tiers; “the fence is the bridge”; the bottom never positively represented; static Riemann-sphere figure. formal:556101b5 |
| Zero Paradox Foreword | v2.14 | Zero_Paradox_Foreword.pdf | N/A | N/A | v2.14: “Rogers’ fixed-point theorem” corrected from “Roger’s” (Hartley Rogers Jr.). ZP-L made this exact correction at its v1.4 and it was never swept to the rest of the corpus; Mathlib carries the same typo upstream at Computability/PartrecCode.lean:36,1001. Prose only, no claim changed.v2.13: T-COMP overclaim corrected (bedrock) - four-way -> three-way, Kleene’s fixed point named as a KleeneStructure assumption not a fourth clause; “DA-1 is closed concretely … grounding the framework in the theory of computation” -> structural half only, self-execution a commitment. v2.12: SYNC TO CLAIMS.md + bedrock false-premise fix (release-prep) — struck “a well-founded ⊥ would admit an external interpreter” (finite-interpretability fallacy, same class as ZP-E v3.24 / ZP-A v1.20), ZFC-incompatibility now on ⊥={⊥} self-membership (no_quine_atom); AX-B1 = the one substantive modeling commitment (not “directly verifiable / not a novel commitment”); MC-1 = the bottom family (not a commitment; identity retired ill-typed), CC-1 derived (ZP-J cc1_derived), CC-2 a Forced Metatheoretic Commitment.v2.10: §IV cited Yanofsky (2003) + Lawvere (1969) for the diagonal-fixed-point unification (prior-art positioning; paired with the new CLAIMS “Convergence with established work” section). C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v2.8: FMC uniformity — CC-2 metatheoretic row “Foundation is ruled out” → “argued to be ruled out”. v2.7: §IV names Lawvere’s fixed-point theorem as the recognized unification of the diagonal family (Cantor/Russell/Gödel fixed-point lemma/Kleene); fence firmed — ZP “locates” the diagonal fixed point, not “is”. v2.6 added the keystone — formal:ab3385c6 |
| ZP Philosophical Question | v1.15 | ZP_Philosophical_Question.pdf | N/A | N/A | v1.15: FORCING OVERCLAIM RETRACTED. The document asserted that T-SNAP establishes the snap OCCURS; it does not. T-SNAP fixes the transition’s shape, and Order/Snap.lean’s NO-GO gauge tsnap_holds_but_nothing_moves proves T-SNAP holds in a model where nothing moves. Occurrence is a framework commitment. Prose only. “You cannot avoid it” asserted occurrence; the surrounding derivability claim (the snap was an axiom, now a theorem) is correct and kept.v1.14: rendered layer COUNT eliminated (project-wide counter removal - “Thirteen formal layers”/”Thirteen layers” de-counted); stale “ZP-A through ZP-M” range dropped from body + endnote.C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.11: fix() guard via Paragraph override; “bridge” → “connecting argument”; “in ZP’s reading” de-duplicated — formal:8df8bb44 |
| ZP Choice-Free Core Addendum | v1.5 | ZP_Choice_Free_Core_Addendum.pdf | N/A | N/A | v1.5: BEDROCK — Section III asserted that the framework has NO PROVEN-NECESSITY CASE ANYWHERE, a universal negative that is FALSE and was live in the published PDF. Two taboo reductions exist: em_of_wellOrder_comparable (comparability of well-orders implies excluded middle; prior art Kraus-Nordvall Forsberg-Xu arXiv:2104.02549 Thm 38(d)) and wem_of_fixedPointFree (the general fixed-point-free principle implies WEAK excluded middle, on the keystone). Neither was named anywhere in this document (0 rendered hits for either). A 2026-08-01 sweep recorded both universal negatives as removed from the corpus — it grepped .lean and missed this Python build script, so the claim survived in RENDERED PUBLIC PROSE. Found 2026-08-03 by the new modal-claim sweep (CLAUDE.md, Prose that resists correction is a CLAIM defect). Section III now states the reduction-vs-measurement distinction, names both cases, and adds the type-vs-proof point: an axiom in a TYPE cannot be removed by any proof, so removability there means changing the statement. Docstring header said 1.3 while VERSION said 1.4 — corrected.v1.4: FORCING OVERCLAIM RETRACTED. The document described the snap as forced with no occurrence hedge. T-SNAP fixes the transition’s SHAPE; tsnap_holds_but_nothing_moves proves it holds in a model where nothing moves, so occurrence is a framework commitment. Prose only. NOTE: this row also carried a STALE hash token that no gate could catch - check_hashes.py had no key for this document (nor for the three ZP-J addenda). All four are now guarded.C8 dual-date templating (Initial/Current meta line; hardcoded month removed).v1.3: rendered Lean-file citations synced to post-reorg basenames (ZPx_* -> ).v1.1: WheelFrac. citation → ZPJ_WheelFrac.* (Lean namespace standardization). v1.0: Initial release — the conceptual core is choice-free; T-SNAP axiom-free; Classical.choice confined to the analytic realizations (inherited from Mathlib); dependence ≠ necessity (open). Anchored on AxiomProfile.lean — formal:72da5de4 |
Comp AR column key: Y/Y = current comp hash adversary-reviewed + remediated (or confirmed clean). Y/N = reviewed, fixes identified but not yet applied. N/— = not yet reviewed.
Script Hash Verification + AR Tracking
The formal:XXXXXXXX comp:XXXXXXXX tokens in the Notes column above are SHA-256 (first 8 chars) fingerprints of the corresponding build scripts in .claude-local/. The Comp AR column tracks adversary-review status for each companion, backed by .claude-local/ar_status.json.
Session start — run once before touching any build script:
python .claude-local/check_hashes.py
A hash MISMATCH means a script was modified without a version bump and PDF rebuild. An AR status of STALE means the companion script changed since its last adversary review — re-review required before merge.
Post-fix workflow — after applying adversary-review fixes, rebuilding the PDF, and updating the hash in register.md, run one command to close the loop:
python .claude-local/check_hashes.py --mark-remediated ZP-X
This computes the current comp hash, writes it to ar_status.json as remediated, and updates the Comp AR column in this file automatically. For fixes identified but not yet applied, use --mark-reviewed ZP-X instead (sets Y/N).