"""
Zero Paradox — ZP-H: Categorical Bridge PDF Builder
Version 1.15 | May 2026
v1.15: CC-1 framing updated — CC-1 is a derived theorem in ZP-J (cc1_derived, Lean 4),
no longer a freestanding modelling commitment.
v1.14: K-13 vocabulary fix — "topological isolation" → "clopen separation" throughout;
updated DP-1 and related prose to use precise vocabulary.
v1.13: Version number removed from Open Items Register section header.
v1.12: Scaffolding note removed from preamble — "ZP-H cannot be written until ZP-G is internally
closed" was a development artifact not appropriate in a public document.
v1.11: Remark R-FORCING added between Sections V and VI — addresses the "renaming" concern;
explains that the four domain functors each independently ground the snap through their own
domain logic, verified sorry-free in Lean 4; structural forcing, not categorical re-description.
v1.10: fc_functor and fd_functor added — F_C and F_D now have concrete Lean Functor terms
(InfoDepth and HilbDimDepth appendices in ZPH.lean). OQ-G3 fully closed for all four functors.
C-H3/C-H4 status, OQ-G3 register, and Validation table updated to reflect sorry-free status.
v1.9: C-H3 AX-G1 no-terminal argument corrected — replaced "larger alphabets" appeal with
Lean-verified argument: ℝ≥0 has no greatest element (t + 1 > t), categorical expression of ZP-A R1.
v1.8: C-H1 AX-G2 verification note added — ⊥-to-0 identification depends on CC-1/DA-2.
v1.7: T-H3 consistency note strengthened — independence of null-analog discovery foregrounded.
v1.5: fb/fc/fd shared witness consolidated into nnreal_initial_grounding.
v1.4: OQ-G3 register updated — fb/fc/fd share proof term nnrealZPCategory.zpIsInitial.
v1.3: T-H3 cross-framework consistency caveat expanded.
v1.1: AX-1 updated to T-SNAP; Import Registry updated to ZP-G v1.1; OQ-G1 closed.
v1.0: Initial release.
"""
import os
from zp_utils import *
VERSION = '1.15'
def label_box_status(title, status_line, rows_list):
"""Box with blue header, italic status sub-row, then content rows."""
data = [
[Paragraph(fix(title), S['label'])],
[Paragraph(fix(status_line), S['cellI'])],
]
for r in rows_list:
data.append([Paragraph(fix(r), S['cell'])])
ts = TableStyle([
('BACKGROUND', (0,0), (-1,0), BLUE),
('BACKGROUND', (0,1), (-1,1), BLUE_LITE),
('BACKGROUND', (0,2), (-1,-1), GREY_LITE),
('TEXTCOLOR', (0,0), (-1,0), WHITE),
('BOX', (0,0), (-1,-1), 0.5, BLUE),
('LINEBELOW', (0,0), (-1,0), 0.5, BLUE),
('LINEBELOW', (0,1), (-1,-2), 0.5, colors.HexColor('#CCCCCC')),
('TOPPADDING', (0,0), (-1,-1), 5),
('BOTTOMPADDING', (0,0), (-1,-1), 5),
('LEFTPADDING', (0,0), (-1,-1), 8),
('RIGHTPADDING', (0,0), (-1,-1), 8),
('VALIGN', (0,0), (-1,-1), 'TOP'),
])
t = Table(data, colWidths=[TW], repeatRows=1)
t.setStyle(ts)
return t
def build():
out_path = os.path.join(PROJECT_ROOT, 'ZP-H_Categorical_Bridge.pdf')
print(f'[build_zph] Output: {out_path}')
doc = make_doc(out_path, 'ZP-H: Categorical Bridge', 'ZP-H: Categorical Bridge',
'Version ' + VERSION, date_str='May 2026')
E = []
print('[build_zph] Building title block...')
# ── TITLE BLOCK ──────────────────────────────────────────────────────────
E += [
sp(12),
Paragraph('THE ZERO PARADOX', S['title']),
Paragraph('ZP-H: Categorical Bridge', S['subtitle']),
Paragraph('Version ' + VERSION + ' | May 2026', S['bodyI']),
sp(8),
hr(),
sp(4),
]
E += [
body('This document connects ZP-G (Category Theory) to ZP-A through ZP-E. Its function is '
'exactly analogous to ZP-E\'s role in the original framework: ZP-E connected the four '
'domain documents to each other; ZP-H connects the categorical generalization back to '
'those four domain documents. Every cross-framework claim is traced to a theorem in '
'ZP-G or ZP-A through ZP-E, plus an explicit bridge axiom where required. No floating '
'connections.'),
body('ZP-H inherits all open items from ZP-G with their original labels. The four open '
'questions from ZP-G — OQ-G1 through OQ-G4 — are the primary targets of this document. '
'OQ-G2, OQ-G3, and OQ-G4 are resolved here. OQ-G1 is resolved in ZP-G via '
'D7\' and I-KC. All four OQ-G items are now closed.'),
body('Sequencing note: ZP-H introduces one new definition (D-H1: the morphisms of C) that '
'was deliberately omitted from ZP-G to keep that document domain-independent. This '
'definition belongs here because it is instantiation-specific: the morphisms of C are '
'defined by what the functor constructions require, not by the abstract category itself.'),
sp(4),
hr(),
]
print('[build_zph] Building Section I: Imported Results...')
# ── I. IMPORTED RESULTS ──────────────────────────────────────────────────
E.append(Paragraph('I. Imported Results', S['h1']))
E.append(Paragraph('1.1 From ZP-G', S['h2']))
E.append(label_box_status(
'Import Registry IR-G — Closed Results from ZP-G v1.1',
'Status: Valid — Received',
[
'D1: Category (objects, morphisms, composition, identity, associativity, unit laws)',
'D2: Morphism uniqueness notation (∃!)',
'D3: Initial object 0 — unique morphism ιX: 0 → X for all X',
'D4: Terminal object — defined for exclusion only',
'D5: Morphism chain from 0',
'D6: Functor — object map, morphism map, preservation of composition and identity',
'D7\': Native categorical surprisal I(f) = K(xB|xA) via I-KC (replaces D7/BA-G1 from v1.0)',
'I-KC: Conditional Kolmogorov complexity K(x|y) imported from ZP-C — named dependency, not bridge axiom',
'AX-G1: Asymmetry Axiom — C has initial object 0, no terminal object',
'AX-G2: Source Asymmetry — hom(X, 0) = ∅ for X ≠ 0',
'R-BA: Leinster categorical entropy characterization [Compatibility Remark — BA-G1 demoted from Bridge Axiom in ZP-G v1.1. No longer a theorem premise.]',
'T1: Initial object unique up to unique isomorphism',
'T2: Universal Constituent — ∀X ∈ ob(C), ∃! ιX: 0 → X',
'T3: Unreachability — hom(X, 0) = ∅ for X ≠ 0',
'T4: Chains are forward-only — no chain returns to 0',
'T5: Functors preserve initial objects [OQ-G2 closed in ZP-H T-H1]',
'T6: Informational singularity of 0 — outward surprisal accumulates; inward undefined [rebuilt in ZP-G v1.1 on D7\'; BA-G1 not a dependency]',
'T7: Categorical Zero Paradox — closing theorem of ZP-G',
'OQ-G1: Closed in ZP-G v1.1 via D7\' (native categorical surprisal) and I-KC (Kolmogorov import from ZP-C). BA-G1 demoted to compatibility remark.',
]
))
E.append(sp(8))
E.append(Paragraph('1.2 From ZP-A through ZP-E', S['h2']))
E.append(label_box_status(
'Import Registry IR-ZP — Closed Results from ZP-A through ZP-E',
'Status: Valid — Received',
[
'From ZP-A: Join-semilattice (L, ∨, ⊥). ⊥ is the unique additive identity. '
'⊥ ≤ x for all x ∈ L (T2). State sequences are monotone (T3). No subtraction operator.',
'From ZP-B: Q2 with ultrametric d. AX-B1 (binary existence). MP-1 (minimality principle). '
'p = 2 derived (T0). Every ball is clopen (T2). Q2 totally disconnected (T5). '
'Clopen separation of 0 from all nonzero elements (T3). Snap irreversibility (C3).',
'From ZP-C: Incompressibility threshold P0 (D1). RP-1 (representation principle). '
'State representations derived from AX-B1 (T1). JSD = 1 bit (T1b). Discrete surprisal operator DF (D5, D6). '
'Non-conservatism of DF on infinite sequences approaching 0 (T2). L-RUN (execution is non-null state change). '
'TQ-IH (no program outputs ⊥ without non-null intermediate state). '
'T-BUF / T-SNAP: Binary Snap derived as theorem.',
'From ZP-D: H = ℂn (D1). T: Q2 → H constructed by basis assignment (T2). '
'T unique up to unitary equivalence (T3). Snap produces orthogonal shift (T4). '
'Monotone sequences map to accumulating vectors (T5). DP-1 (orthogonality design commitment).',
'From ZP-E: Universal constituent cross-framework (T1). Hamming/JSD consistency (T2). '
'Landauer bridge BA-1. Processing bounds T3. Unified Snap description T4. '
'Iterative forcing T5. State representations T6. Zero Paradox T7. '
'T-SNAP: Binary Snap is a derived theorem — AX-1 is not an axiom.',
]
))
E.append(sp(8))
E.append(label_box_status(
'Inherited Labels Registry IR-2 — Open Items Carried into ZP-H',
'Status: Structural — labels preserved without laundering',
[
'OQ-G1 [Closed in ZP-G v1.1]: Native derivation of categorical surprisal without importing Shannon entropy. '
'Closed by D7\' (conditional Kolmogorov complexity K(B|A)) and I-KC. BA-G1 demoted to compatibility remark R-BA.',
'OQ-G2 [Resolved in Section IV]: Left adjoint verification for instantiation functors.',
'OQ-G3 [Resolved in Section III]: Explicit construction of four instantiation functors.',
'OQ-G4 [Resolved in Section V]: Reconciliation of categorical and ZP-C singularity characterizations.',
]
))
print('[build_zph] Building Section II: Morphisms of C...')
# ── II. THE MORPHISMS OF C ────────────────────────────────────────────────
E.append(Paragraph('II. The Morphisms of C — New Definition', S['h1']))
E += [
body('ZP-G defined C abstractly: objects, morphisms, composition, identity, satisfying the '
'category axioms plus AX-G1 and AX-G2. The morphisms of C were left unspecified '
'because the abstract results (T1 through T7) require only the categorical axioms, not a '
'concrete description of what morphisms are. That abstraction was correct for ZP-G.'),
body('ZP-H requires concreteness. To construct the instantiation functors, we must specify '
'what morphisms of C are, so that we can say what the functor maps them to. That '
'specification belongs here, not in ZP-G.'),
]
E.append(label_box_status(
'Definition D-H1 — Morphisms of C — State Transitions',
'Status: Definition — instantiation-specific',
[
'A morphism f: A → B in C is a state transition: a structure-preserving map from state A to state B satisfying:',
'(i) Forward direction: Every morphism f: A → B represents a net addition of informational content. '
'No morphism reduces state.',
'(ii) Compatibility with AX-G2: For any non-initial object X ≠ 0, no morphism X → 0 exists. D-H1(i) '
'and AX-G2 are consistent: a net-additive transition cannot return to the minimal state 0.',
'(iii) Composition: Composition of morphisms corresponds to sequential state accumulation. f: A → B '
'followed by g: B → C produces a state at least as large as B.',
'Status note: D-H1 is a design commitment, not a derivation. It is the choice that makes the '
'instantiation functors well-defined. A different choice of morphism structure would yield different '
'functors. D-H1 is the choice that maps correctly to all four ZP domain documents.',
]
))
print('[build_zph] Building Section III: Instantiation Functors...')
# ── III. CONSTRUCTION OF THE INSTANTIATION FUNCTORS ──────────────────────
E.append(Paragraph('III. Construction of the Instantiation Functors [OQ-G3: PDF Constructions Complete]', S['h1']))
E += [
body('ZP-G Remark R3 claimed the existence of four functors FA, FB, FC, FD without '
'constructing them. This section constructs all four. Each construction must specify the '
'object map, the morphism map, and verify preservation of composition and identity. Each '
'must also show that AX-G1 and AX-G2 are respected.'),
]
E.append(Paragraph('3.1 FA: C → SLat (Join-Semilattices)', S['h2']))
E.append(label_box_status(
'Construction C-H1 — Functor FA: C → SLat',
'Status: Derived — OQ-G3 partially closed',
[
'Object map: FA sends each object X ∈ ob(C) to the state SX ∈ L in the '
'join-semilattice (L, ∨, ⊥) of ZP-A. The initial object 0 maps to ⊥: FA(0) = ⊥.',
'Morphism map: FA sends each morphism f: A → B to the join operation that witnesses the '
'transition: FA(f) = (SA ∨ α) for some α ∈ L such that SA ∨ α = SB. '
'By ZP-A D2, every valid state transition is a join.',
'Preservation of composition: For f: A → B and g: B → C, FA(g ∘ f) = SA ∨ αf ∨ αg = '
'FA(g) ∘ FA(f) by associativity of ∨ (ZP-A A1). ✓',
'Preservation of identity: FA(idA) = SA ∨ ⊥ = SA by ZP-A A4 (additive identity). ✓',
'AX-G1 respected: FA(0) = ⊥ is the global minimum of L (ZP-A T2). No element of SLat is a terminal '
'object because L has no top element ⊤ (ZP-A R1). ✓',
'AX-G2 respected: No join operation in L can return to ⊥ from a strictly larger state (ZP-A T3, '
'monotonicity). Therefore FA sends no non-initial morphism to a map terminating at ⊥. '
'Note: this verification depends on CC-1 / DA-2 to identify L\'s ⊥ with C\'s initial object 0. '
'CC-1 is a derived theorem in ZP-J (cc1_derived, Lean 4) within the ZF+AFA setting — no longer a freestanding modelling commitment. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('3.2 FB: C → pTop (p-Adic Topological Spaces)', S['h2']))
E.append(label_box_status(
'Construction C-H2 — Functor FB: C → pTop',
'Status: PDF construction complete — Lean: full functor (fb_functor, sorry-free)',
[
'Object map: FB sends each object X ∈ ob(C) to an element x ∈ Q2. The initial object 0 maps to '
'the element 0 ∈ Q2: FB(0) = 0 ∈ Q2.',
'Morphism map: FB sends each morphism f: A → B to the discrete jump from xA to xB '
'in Q2. By ZP-B T2, any two distinct elements of Q2 lie in disjoint clopen balls. The jump is across a clopen '
'boundary — a well-defined topological transition.',
'Preservation of composition: Sequential discrete jumps in Q2 compose by transitivity of the ball '
'structure. xA → xB → xC is a valid sequence of clopen transitions. ✓',
'Preservation of identity: FB(idA) is the trivial jump xA → xA, which is the identity on Q2. ✓',
'AX-G1 respected: FB(0) = 0 ∈ Q2 is clopen-separated from all nonzero elements (ZP-B T3). No terminal object exists in '
'pTop because Q2 is totally disconnected (ZP-B T5) — there is no single element to which all paths converge. ✓',
'AX-G2 respected: ZP-B C3 establishes that no continuous path in Q2 returns to 0 from any '
'non-zero element. FB maps no non-initial morphism to a transition terminating at 0 ∈ Q2. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('3.3 FC: C → InfoSp (Information-Theoretic Spaces)', S['h2']))
E.append(label_box_status(
'Construction C-H3 — Functor FC: C → InfoSp',
'Status: PDF construction complete — Lean: full functor (fc_functor, sorry-free)',
[
'Object map: FC sends each object X ∈ ob(C) to a probability distribution PX over {0, 1}. The initial '
'object 0 maps to the Null State distribution: FC(0) = P = (1, 0) (derived from AX-B1 and RP-1 in ZP-C T1).',
'Morphism map: FC sends each morphism f: A → B to the informational transition from PA to PB, '
'with informational work E = JSD(PA ∥ PB) ≥ 0. The fundamental transition (0 → first non-initial '
'object) maps to JSD(P ∥ Q) = 1 bit (ZP-C T1b).',
'Preservation of composition: In the binary framework (two outcome states), only two non-trivial distributions exist: '
'P = (1, 0) and Q = (0, 1). The snap f: 0 → ε0 is the unique morphism mapping P → Q at cost '
'JSD(P ∥ Q) = 1 bit. All successor morphisms g: εn → εn+1 map Q → Q (Q-stability of the '
'post-snap codomain), giving FC(g) = JSD(Q ∥ Q) = 0. Therefore FC(g ∘ f) = 1 bit = '
'FC(g) + FC(f) = 0 + 1 bit. Composition is preserved exactly by Q-stability, not by '
'subadditivity. (Note: JSD subadditivity is an inequality and does not establish this — '
'the equality holds here as a structural consequence of the binary framework.) ✓',
'Preservation of identity: FC(idA) = JSD(PA ∥ PA) = 0. No informational work is done by a trivial transition. ✓',
'AX-G1 respected: The Null State P = (1, 0) is the unique distribution of minimum entropy (H(P) = 0 bits). '
'No terminal object exists: the shared NNRealZPCat witness (ℝ≥0 with ≤) has no greatest element '
'— t + 1 > t for all t ≥ 0 — so no terminal object can exist in the ordered structure. '
'This is the categorical expression of ZP-A R1 (no top element), applied to the concrete model. '
'Verified in Lean: ax_g1_no_terminal (nnrealZPCategory). ✓',
'AX-G2 respected: JSD ≥ 0. A transition returning to P = (1, 0) from any Q ≠ P would require JSD(Q ∥ P) = 0, '
'which holds only if Q = P. Since Q ≠ P by assumption, no such transition exists. ✓',
'Inherited label: The distributions P = (1, 0) and Q = (0, 1) are derived from AX-B1 and RP-1 (ZP-C T1, ZP-E T6). '
'All results depending on FC inherit the AX-B1 and RP-1 labels.',
]
))
E.append(sp(6))
E.append(Paragraph('3.4 FD: C → Hilb (Hilbert Spaces)', S['h2']))
E.append(label_box_status(
'Construction C-H4 — Functor FD: C → Hilb',
'Status: PDF construction complete — Lean: full functor (fd_functor, sorry-free)',
[
'Object map: FD sends each object X ∈ ob(C) to a state vector T(x) ∈ H = ℂn via the transition '
'operator T: Q2 → H constructed in ZP-D (T2). The initial object 0 maps to: FD(0) = T(0) = e0.',
'Morphism map: FD sends each morphism f: A → B to the orthogonal extension from T(xA) to T(xB) '
'in H. By ZP-D T4, distinct elements of Q2 map to orthogonal basis vectors under T, so the transition is a well-defined orthogonal step in H.',
'Preservation of composition: Sequential orthogonal extensions compose by accumulation: T(xA) → T(xB) → '
'T(xC) produces ‖T(xC)‖ ≥ ‖T(xB)‖ ≥ ‖T(xA)‖ by ZP-D T5. ✓',
'Preservation of identity: FD(idA) maps to the trivial orthogonal extension T(xA) → T(xA), which is the identity on the basis vector ek. ✓',
'AX-G1 respected: FD(0) = e0 is the anchor vector from which all other state vectors are orthogonal '
'extensions (ZP-D T3). No terminal object exists in Hilb under this construction because the orthogonal extension sequence is unbounded in norm (ZP-D T5). ✓',
'AX-G2 respected: ZP-D T4 establishes that the Snap produces an orthogonal shift that cannot be '
'reversed without violating the additive ontology (ZP-A R1). No orthogonal extension terminates back at e0 from a non-initial vector. ✓',
'Design commitment inherited: DP-1 (orthogonality as representation of clopen separation) is a '
'design commitment in ZP-D v1.2. FD inherits this label. T4 and T5 of ZP-D depend on DP-1 as a premise.',
]
))
print('[build_zph] Building Section IV: Left Adjoint Verification...')
# ── IV. LEFT ADJOINT VERIFICATION ────────────────────────────────────────
E.append(Paragraph('IV. Left Adjoint Verification [OQ-G2 Closed]', S['h1']))
E += [
body('ZP-G T5 stated that functors preserve initial objects, but marked it conditional on OQ-G2: '
'verifying that the instantiation functors are left adjoints (or otherwise preserve the '
'universal property of 0 fully, not just for objects in their image). This section closes OQ-G2.'),
]
E.append(label_box_status(
'Theorem T-H1 — Each Instantiation Functor Preserves the Initial Object',
'Status: Derived — OQ-G2 closed',
[
'Claim: For each functor F ∈ {FA, FB, FC, FD}, F(0) is an initial object in the codomain category.',
'Strategy: Rather than proving each functor is a left adjoint in full generality (which would require '
'establishing adjoint pairs for SLat, pTop, InfoSp, and Hilb), we verify the universal property '
'directly for each functor. The universal property of the initial object requires: for every object Y in '
'the codomain, ∃! morphism F(0) → Y.',
'FA: FA(0) = ⊥. For any SY ∈ L, the unique morphism ⊥ → SY is the join ⊥ ∨ SY = SY (ZP-A A4). '
'Uniqueness: ⊥ is the global minimum (ZP-A T2), so the only order-preserving map from ⊥ to SY is the join with SY. ✓',
'FB: FB(0) = 0 ∈ Q2. For any x ∈ Q2, the unique morphism 0 → x is the discrete jump from 0 to x '
'across the clopen boundary. Uniqueness: 0 is clopen-separated from all nonzero elements (ZP-B T3); the only clopen-respecting transition from 0 to x is the direct jump. ✓',
'FC: FC(0) = P = (1, 0). For any distribution PY, the unique morphism P → PY is the informational '
'transition with work E = JSD(P ∥ PY). Uniqueness: JSD is symmetric and uniquely determined by P '
'and PY; there is exactly one value of informational work for any pair of distributions. ✓',
'FD: FD(0) = T(0) = e0. For any T(x) ∈ H, the unique morphism e0 → T(x) is the orthogonal extension '
'from e0 to ek (the basis vector assigned to x). Uniqueness: T is unique up to unitary equivalence '
'(ZP-D T3); the orthogonal extension is unique up to the same equivalence. ✓',
'Conclusion: OQ-G2 is closed. ZP-G T5 is now unconditional for the four instantiation functors '
'of this framework. The universal property of 0 ∈ ob(C) is fully preserved under FA, FB, FC, and FD. ✓',
]
))
print('[build_zph] Building Section V: Singularity Reconciliation...')
# ── V. SINGULARITY RECONCILIATION ────────────────────────────────────────
E.append(Paragraph('V. Singularity Reconciliation [OQ-G4 Closed]', S['h1']))
E += [
body('ZP-G T6 characterized the informational singularity of 0 as an undefined domain: the '
'categorical surprisal I(X → 0) is undefined because no such morphism exists. ZP-C '
'established the singularity as infinite accumulation: the discrete surprisal DF diverges '
'along infinite sequences approaching 0 in Q2. ZP-G R4 claimed these are compatible but '
'did not prove it. This section closes OQ-G4.'),
]
E.append(label_box_status(
'Theorem T-H2 — Compatibility of Singularity Characterizations',
'Status: Derived — OQ-G4 closed',
[
'Claim: The categorical singularity (undefined domain, ZP-G T6) and the ZP-C singularity (infinite '
'accumulation, ZP-C T2) are compatible characterizations of the same structural fact under the functor FC.',
'Setup: Let {Xn} be a sequence of objects in C such that the corresponding sequence {FC(Xn)} = '
'{Pn} in InfoSp approaches FC(0) = P = (1, 0) in distribution. Under FB, the corresponding '
'sequence {xn} in Q2 approaches 0 ∈ Q2.',
'ZP-C side: By ZP-C T2, the discrete surprisal DF along the infinite sequence {xn} approaching 0 in '
'Q2 is non-conservative: the accumulated surprisal ∑ DF(xk → xk+1) diverges as n → ∞. The singularity is infinite accumulation.',
'ZP-G side: By ZP-G T6(ii), I(X → 0) is undefined for all X ≠ 0 because hom(X, 0) = ∅ (AX-G2). The singularity is undefined domain.',
'Reconciliation: These are two descriptions of the same obstruction from different vantage points. '
'In ZP-C, we ask: what happens to surprisal as we approach 0 along an infinite sequence? The '
'answer is divergence — the accumulation is unbounded. In ZP-G, we ask: can we reach 0 by a '
'morphism from outside? The answer is no — the morphism does not exist. Divergence and '
'non-existence are consistent: if the accumulation required to reach 0 is infinite, then no finite '
'morphism can accomplish it, which is exactly the statement hom(X, 0) = ∅. The undefined-domain '
'condition in ZP-G is the categorical expression of the infinite-accumulation condition in ZP-C. ✓',
'Precise statement: Under FC, the statement hom(X, 0) = ∅ in C corresponds to the statement that '
'no finite informational path from PX to P = (1, 0) has finite total surprisal — which is exactly the '
'content of ZP-C T2 restricted to finite paths. OQ-G4 is closed. ✓',
]
))
E.append(remark_box(
'Remark R-FORCING — Structural Forcing vs. Re-Description [new in v1.11]',
[
'The four functors (FA, FB, FC, FD) established in '
'Sections III-V do not merely translate the Binary Snap into categorical language. Each functor '
'independently grounds the snap in its own domain: FA shows the lattice join forces '
'ε0 above ⊥; FB shows the 2-adic topology forces an irreversible '
'jump at 0; FC shows the information-theoretic transition costs exactly 1 bit; '
'FD shows the Hilbert space snap is an orthogonal shift.',
'That the same structural singularity appears across four independently grounded domain categories '
'— each confirmed sorry-free in Lean 4 (fb_snap_q2_grounded, fc_snap_info_grounded, '
'fd_snap_hilb_grounded) — is not re-description. It is the theorem: the phenomenon is '
'structurally forced across all four canonical mathematical languages for state description.',
]
))
print('[build_zph] Building Section VI: Binary Snap...')
# ── VI. THE BINARY SNAP — CATEGORICAL DESCRIPTION ────────────────────────
E.append(Paragraph('VI. The Binary Snap — Categorical Description', S['h1']))
E.append(label_box_status(
'Theorem T-H3 — The Binary Snap Under All Four Functors',
'Status: Derived — Cross-Framework',
[
'Setup: The Binary Snap is the transition from 0 ∈ ob(C) to the first non-initial object '
'ε0 ∈ ob(C), driven by the incompressibility threshold P0 (ZP-C D1) under '
'T-SNAP (Binary Snap — Derived Theorem, ZP-E v2.0).',
'In C (ZP-G): The Snap is the morphism ιε0: 0 → ε0. By D3, this morphism is unique. '
'By T4, no chain returns from ε0 to 0. The Snap is categorically irreversible.',
'Under FA (ZP-A): FA(ιε0) = ⊥ ∨ ε0 = S1. The Snap is the first join. Monotone and irreversible by ZP-A T3. '
'T-SNAP is a derived theorem (ZP-E v2.0); inherited here with derived status.',
'Under FB (ZP-B): FB(ιε0) is the discrete jump 0 → ε0 ∈ Q2 across a clopen boundary (ZP-B T2). '
'Topologically irreversible by ZP-B C3.',
'Under FC (ZP-C): FC(ιε0) is the informational transition P → Q with E = JSD(P ∥ Q) = 1 bit (ZP-C '
'T1b). Irreversible: JSD(Q ∥ P) = 1 bit ≠ 0.',
'Under FD (ZP-D): FD(ιε0) is the orthogonal shift T(0) = e0 → T(ε0) = e1. '
'⟨e0, e1⟩ = 0 (ZP-D T4). Norm-increasing (ZP-D T5). DP-1 is a design premise.',
'Cross-framework consistency: All four functors agree that the Snap is irreversible. Each '
'irreversibility result is a closed theorem within its own domain document. Their agreement is '
'structural consistency, not circular argument. Independence of null-analog discovery: each '
'framework located its null-analog through its own domain logic — ⊥ through A4 (ZP-A), '
'0 ∈ Q2 through T3 (ZP-B), P = (1,0) through D1/RP-1 (ZP-C), e0 through '
'T2/T3 (ZP-D) — prior to and without reference to the others. The modeling commitment is the '
'identification of these independently-located objects under the functors, not the claim that '
'any domain forced the others\' choices. Their agreement confirms coherence across mathematical '
'representations of a shared foundation, not external replication. '
'T-SNAP (Binary Snap Causality) is a derived '
'theorem in ZP-E v2.0 and is inherited here with derived status. DP-1 remains the only design premise. ✓',
]
))
print('[build_zph] Building Section VII: Traceability Register...')
# ── VII. FULL TRACEABILITY REGISTER ──────────────────────────────────────
E.append(Paragraph('VII. Full Traceability Register', S['h1']))
E += [
body('Every cross-framework claim in ZP-H is traced here to its grounding theorem and any required bridge axiom.'),
]
trace_rows = [
['FA(0) = ⊥', 'ZP-A T2; C-H1', 'None', 'Valid — Derived'],
['FA preserves composition', 'ZP-A A1; C-H1', 'None', 'Valid — Derived'],
['FA respects AX-G1, AX-G2', 'ZP-A T2, T3, R1; C-H1', 'None', 'Valid — Derived'],
['FB(0) = 0 ∈ Q2','ZP-B T3; C-H2', 'None', 'Valid — Derived'],
['FB preserves composition', 'ZP-B T2; C-H2', 'None', 'Valid — Derived'],
['FB respects AX-G1, AX-G2', 'ZP-B T5, C3; C-H2', 'None', 'Valid — Derived'],
['FC(0) = P = (1,0)', 'ZP-C T1; ZP-E T6; C-H3', 'AX-B1, RP-1', 'Valid — from AX-B1, RP-1'],
['FC preserves composition', 'Q-stability of post-snap codomain; C-H3', 'None', 'Valid — Derived (binary framework; Q-stability, not subadditivity)'],
['FC respects AX-G1, AX-G2', 'ZP-C T1b; C-H3', 'AX-B1, RP-1', 'Valid — from AX-B1, RP-1'],
['FD(0) = T(0) = e0', 'ZP-D T2, T3; C-H4', 'DP-1', 'Valid — from DP-1'],
['FD preserves composition', 'ZP-D T5; C-H4', 'DP-1', 'Valid — from DP-1'],
['FD respects AX-G1, AX-G2', 'ZP-D T4, T5; C-H4', 'DP-1', 'Valid — from DP-1'],
['T-H1: universal property preserved', 'ZP-A T2; ZP-B T3; ZP-C T1b; ZP-D T3', 'None', 'Valid — OQ-G2 closed'],
['T-H2: singularity compatibility', 'ZP-G T6; ZP-C T2; C-H3', 'None', 'Valid — OQ-G4 closed'],
['T-H3: Snap under all four functors', 'C-H1 through C-H4; ZP-E T4; ZP-E T-SNAP', 'DP-1', 'Valid — T-SNAP derived (ZP-E v2.0)'],
['D-H1: morphisms of C', 'ZP-A D2; ZP-B T2; ZP-C; ZP-D', 'None', 'Design Commitment'],
]
E.append(data_table(
['Claim', 'Grounded In', 'Bridge Axiom?', 'Status'],
trace_rows,
[TW*0.25, TW*0.35, TW*0.17, TW*0.23]
))
print('[build_zph] Building Section VIII: Open Items Register...')
# ── VIII. OPEN ITEMS REGISTER ─────────────────────────────────────────────
E.append(Paragraph('VIII. Open Items Register', S['h1']))
oq_rows = [
['OQ-G1',
'Closed — ZP-G v1.1\nD7\', T6',
'Native derivation of categorical surprisal without importing Shannon entropy. '
'Closed in ZP-G v1.1 by D7\' (native categorical surprisal K(B|A)) and I-KC '
'(Kolmogorov import from ZP-C). BA-G1 demoted to compatibility remark R-BA. '
'No bridge axiom remains as a theorem premise.'],
['OQ-G2',
'Closed — T-H1',
'Left adjoint verification for instantiation functors. Resolved in Section IV by '
'direct verification of the universal property for each of the four functors.'],
['OQ-G3',
'Closed — all four\nfunctors (Lean)',
'PDF-level constructions of all four instantiation functors complete (Section III). '
'All four now have concrete Lean Functor terms (sorry-free): '
'FA: fa via NatSLat (Functor ℕ ℕ, effectively). '
'FB: fb_functor (Functor ℕ Q₂BallDepth), snap grounded in C3. '
'FC: fc_functor (Functor ℕ InfoDepth), snap grounded in T1b. '
'FD: fd_functor (Functor ℕ HilbDimDepth), snap grounded in T4. '
'Each domain type has a distinct ZPCategory instance and preserves_initial definition. '
'OQ-G3 fully closed.'],
['OQ-G4',
'Closed — T-H2',
'Reconciliation of categorical (undefined domain) and ZP-C (infinite accumulation) '
'singularity characterizations. Resolved in Section V. The two characterizations '
'are shown to be the same obstruction described from different vantage points.'],
['AX-1',
'Derived —\nT-SNAP\n(ZP-E v2.0)',
'Binary Snap Causality. Derived as Theorem T-SNAP in ZP-E v2.0 via the '
'P₀ / L-RUN / TQ-IH / DA-1 chain. No longer an axiom. T-H3 inherits '
'T-SNAP as a derived result. Not a gap.'],
['AX-G1',
'Axiom —\nnot novel',
'Asymmetry: initial object 0, no terminal object. Inherited from ZP-G. '
'Not a novel commitment — grounded in ⊥ as bottom element of ZP-A semilattice. Not a gap.'],
['AX-G2',
'Axiom —\nnot novel',
'Source asymmetry: hom(X, 0) = ∅ for X ≠ 0. Inherited from ZP-G. '
'Not a novel commitment — follows from ZP-A antisymmetry and ZP-B C3. Not a gap.'],
['R-BA',
'Remark —\nBA-G1 demoted\n(ZP-G v1.1)',
'Leinster Shannon entropy characterization. BA-G1 demoted from Bridge Axiom '
'in ZP-G v1.0 to Compatibility Remark R-BA in ZP-G v1.1. '
'Derivable from D7\' and I-KC via the coding theorem. Not a gap.'],
['D-H1',
'Design\nCommitment —\nintentional',
'Morphisms of C defined as state transitions. This is a design choice that makes '
'the instantiation functors well-defined. A different morphism structure would yield '
'different functors. Explicitly stated and not laundered as a derivation.'],
['DP-1',
'Design\nCommitment —\ninherited',
'Orthogonality as representation of clopen separation. Inherited from ZP-D v1.1. '
'FD and T-H3 depend on it as a premise.'],
]
E.append(data_table(
['Item', 'Status', 'Description'],
oq_rows,
[TW*0.12, TW*0.18, TW*0.70]
))
print('[build_zph] Building Section IX: Validation Status...')
# ── IX. VALIDATION STATUS ─────────────────────────────────────────────────
E.append(Paragraph('IX. Validation Status', S['h1']))
val_rows = [
['IR-G: ZP-G v1.1 results imported',
'Valid — all ZP-G v1.1 closed results received; labels preserved. '
'BA-G1 demoted to R-BA; I-KC noted as named dependency.'],
['IR-ZP: ZP-A through ZP-E imported',
'Valid — all closed results received from ZP-A through ZP-E; labels preserved. '
'T-SNAP (ZP-E v2.0) noted: AX-1 is derived, not axiomatic.'],
['IR-2: Inherited labels preserved',
'Valid — OQ-G1 closed in ZP-G v1.1; OQ-G2, OQ-G3, OQ-G4 resolved here; '
'BA-G1 updated to R-BA; AX-1 updated to T-SNAP (Derived).'],
['D-H1: Morphisms of C',
'Design Commitment — explicitly stated; required for functor construction'],
['C-H1: FA: C → SLat',
'Valid — Derived. Object map, morphism map, composition, identity all verified. ✓'],
['C-H2: FB: C → pTop',
'Valid — all four requirements verified. Lean: full functor (fb_functor, sorry-free). ✓'],
['C-H3: FC: C → InfoSp',
'Valid — from AX-B1, RP-1; all four requirements verified. Lean: full functor (fc_functor, sorry-free). ✓'],
['C-H4: FD: C → Hilb',
'Valid — from DP-1; all four requirements verified. Lean: full functor (fd_functor, sorry-free). ✓'],
['T-H1: Universal property preserved',
'Valid — OQ-G2 closed. ZP-G T5 is now unconditional for all four instantiation functors. ✓'],
['T-H2: Singularity reconciliation',
'Valid — OQ-G4 closed. Categorical (undefined domain) and ZP-C (infinite accumulation) '
'shown to be the same obstruction under FC. ✓'],
['T-H3: Snap under all four functors',
'Valid — Derived; cross-framework. T-SNAP inherited as derived theorem (ZP-E v2.0). '
'DP-1 labelled as design premise. ✓'],
['Traceability register',
'Valid — Complete. Every cross-framework claim traced to source theorem and bridge axiom. No floating connections.'],
['OQ-G1: Native surprisal derivation',
'Closed in ZP-G v1.1 via D7\' and I-KC. No bridge axiom remains as a theorem premise.'],
['AX-1 (Binary Snap Causality)',
'Derived — T-SNAP in ZP-E v2.0. No longer an axiom. '
'T-H3 and all downstream results inherit the derived status.'],
['AX-G1, AX-G2',
'Not novel commitments — grounded in prior layers (ZP-A and ZP-B). Stated as local axioms in ZP-G for self-containment. Not gaps.'],
['R-BA, D-H1, DP-1',
'Compatibility Remark / Design Commitments — intentional. Explicitly stated. Not laundered.'],
]
E.append(data_table(
['Component', 'Status / Notes'],
val_rows,
[TW*0.35, TW*0.65]
))
E += [
sp(12),
Paragraph(
'End of ZP-H v1.14 | Four instantiation functors constructed | '
'OQ-G1 through OQ-G4 closed | '
'All four functors have concrete Lean Functor terms (sorry-free): '
'fb_functor (Q₂BallDepth), fc_functor (InfoDepth), fd_functor (HilbDimDepth), FA via NatSLat | '
'OQ-G3 fully closed | '
'T-SNAP inherited as derived theorem | '
'T-H3 independence-of-discovery note: null-analog in each domain located independently | '
'No novel axioms: AX-B1 decidable, AX-G1 and AX-G2 grounded in prior layers',
S['note']),
]
print(f'[build_zph] Calling doc.build() with {len(E)} elements...')
doc.build(E)
print(f'[build_zph] Written: {out_path}')
if __name__ == '__main__':
build()