""" Build ZP-L Illustrated Companion Version 1.4 | May 2026 v1.4: Strip version number from companion footer. v1.3: Add "Convergence with Proof Theory" section — Gentzen (1936), ε₀ as PA's proof-theoretic ordinal, structural alignment with ZPL's independent derivation. v1.2: Strip version number from disclaimer cross-reference to ZP-L formal document. v1.0: Initial release. Covers ε₀ as the ordinal snap threshold, 2-adic tower convergence, and Kleene-ordinal structural homology. v1.1: Adversary review fixes — 6 precision corrections: removed grand-unification phrasing ("same object at the bottom of every formal language"), corrected Kleene fixed-point gloss, rewrote Classical.choice parallel as open question per ZPL §I, fixed "from above" p-adic directional error, removed opaque ZPM jargon from example box, changed "independently proved" to "jointly established", updated key result box. Formal doc: ZP-L Incomputability Convergence v1.0. """ import os from zp_utils import * from reportlab.graphics.shapes import Drawing, Line, String, Rect, Circle from reportlab.graphics import renderPDF def snap_tower_diagram(): """Horizontal: tower stages (c0) climbing toward ε₀; snap to c1 at ε₀.""" # dh = 155 pts (≈ 2.15 × 72); box_cy = 88 fixed. # Box top = 88+17 = 105. SNAP label at 105+8 = 113. Header at 105+20 = 125. # Encoding labels at 71-18 = 53. Caption at 10. # Content: top = 125 < 145 (dh-10). Bottom = 10 > 5. ✓ dw, dh = TW, 155 d = Drawing(dw, dh) bw, bh = 60, 34 spacing = 12 box_cy = 88 # fixed — does not derive from dh box_by = box_cy - bh // 2 # = 71 # Stage labels (raw Unicode — String() does not parse HTML entities) stage_labels = ['0', '1', 'ω', 'ω^ω'] # 0, 1, ω, ω^ω n = len(stage_labels) stages_w = n * bw + (n - 1) * spacing # 4×60 + 3×12 = 276 dots_w = 30 gap_w = 22 eps_bw = 62 total_w = stages_w + dots_w + gap_w + eps_bw # = 390 x0 = (dw - total_w) / 2 # ≈ 39 pts # ── Stage boxes (teal) ─────────────────────────────────────────────────── for i, lbl in enumerate(stage_labels): bx = x0 + i * (bw + spacing) d.add(Rect(bx, box_by, bw, bh, fillColor=TEAL_LITE, strokeColor=TEAL, strokeWidth=1.2, rx=3, ry=3)) lbl_x = bx + max(4, (bw - len(lbl) * 6) / 2) d.add(String(lbl_x, box_by + bh - 14, lbl, fontSize=9.5, fontName='DV-B', fillColor=TEAL)) d.add(String(bx + bw / 2 - 7, box_by + 7, 'c0', fontSize=8, fontName='DV-I', fillColor=GREY_TEXT)) if i < n - 1: d.add(Line(bx + bw + 2, box_cy, bx + bw + spacing - 2, box_cy, strokeColor=TEAL, strokeWidth=1.0)) # ── Continuation dots ──────────────────────────────────────────────────── dots_x = x0 + stages_w + 6 for j in range(3): d.add(Circle(dots_x + j * 9, box_cy, 2.5, fillColor=TEAL, strokeColor=TEAL, strokeWidth=0)) # ── Arrow from dots to ε₀ box ──────────────────────────────────────────── eps_bx = x0 + stages_w + dots_w + gap_w arr_x1 = dots_x + 3 * 9 + 6 arr_x2 = eps_bx - 3 d.add(Line(arr_x1, box_cy, arr_x2, box_cy, strokeColor=AMBER, strokeWidth=1.5)) d.add(Line(arr_x2, box_cy, arr_x2 - 7, box_cy + 4, strokeColor=AMBER, strokeWidth=1.5)) d.add(Line(arr_x2, box_cy, arr_x2 - 7, box_cy - 4, strokeColor=AMBER, strokeWidth=1.5)) # ── ε₀ box (amber — snap point) ────────────────────────────────────────── d.add(Rect(eps_bx, box_by, eps_bw, bh, fillColor=AMBER_LITE, strokeColor=AMBER, strokeWidth=1.8, rx=3, ry=3)) # ε as large glyph, 0 as subscript-positioned smaller glyph d.add(String(eps_bx + 12, box_by + bh - 13, 'ε', fontSize=12, fontName='DV-B', fillColor=AMBER)) d.add(String(eps_bx + 22, box_by + bh - 17, '0', fontSize=8, fontName='DV-B', fillColor=AMBER)) d.add(String(eps_bx + eps_bw / 2 - 7, box_by + 7, 'c1', fontSize=8.5, fontName='DV-B', fillColor=AMBER)) # ── "SNAP" label above the transition arrow ─────────────────────────────── snap_label_x = arr_x1 + (arr_x2 - arr_x1) / 2 - 14 d.add(String(snap_label_x, box_by + bh + 8, 'SNAP', fontSize=7.5, fontName='DV-B', fillColor=AMBER)) # ── Caption (raw Unicode — no HTML entities) ────────────────────────────── d.add(String(14, 10, 'Each tower stage is strictly below ε-zero and maps to c0. ' 'The snap to c1 occurs exactly at ε-zero.', fontSize=7.5, fontName='DV-I', fillColor=GREY_TEXT)) return d def dual_convergence_diagram(): """Two rows: ordinal tower approaching ε₀ (top) and 2-adic norms converging to 0 (bottom).""" # dh = 190 pts. row_top = 148 fixed, row_bot = 68 fixed. # Top box top = 148+16 = 164. Top row label at 164+8 = 172 < 180 (dh-10). ✓ # Bottom box bottom = 68-16 = 52. Caption at 10. ✓ dw, dh = TW, 190 d = Drawing(dw, dh) bw, bh = 58, 32 spacing = 12 row_top = 148 # ordinal row center (fixed) row_bot = 68 # 2-adic row center (fixed) # Four corresponding stage columns stage_ord = ['1', 'ω', 'ω^ω', 'ω^ω^ω'] stage_norm = ['1/2', '1/4', '1/8', '1/16'] # 2-adic norms ||2^n||_2 n = len(stage_ord) stages_w = n * bw + (n - 1) * spacing # 4×58 + 3×12 = 268 dots_w = 28 gap_w = 22 end_bw = 62 total_w = stages_w + dots_w + gap_w + end_bw # = 380 x0 = (dw - total_w) / 2 # ≈ 44 pts top_by = row_top - bh // 2 # = 132 bot_by = row_bot - bh // 2 # = 52 # ── Ordinal row (top, teal) ─────────────────────────────────────────────── for i, lbl in enumerate(stage_ord): bx = x0 + i * (bw + spacing) d.add(Rect(bx, top_by, bw, bh, fillColor=TEAL_LITE, strokeColor=TEAL, strokeWidth=1.2, rx=3, ry=3)) lbl_x = bx + max(4, (bw - len(lbl) * 5.5) / 2) d.add(String(lbl_x, top_by + bh - 13, lbl, fontSize=9, fontName='DV-B', fillColor=TEAL)) if i < n - 1: d.add(Line(bx + bw + 2, row_top, bx + bw + spacing - 2, row_top, strokeColor=TEAL, strokeWidth=1.0)) # Ordinal dots dots_x = x0 + stages_w + 5 for j in range(3): d.add(Circle(dots_x + j * 8, row_top, 2, fillColor=TEAL, strokeColor=TEAL, strokeWidth=0)) # Arrow to ε₀ box end_bx = x0 + stages_w + dots_w + gap_w arr1_x1 = dots_x + 3 * 8 + 4 arr1_x2 = end_bx - 3 d.add(Line(arr1_x1, row_top, arr1_x2, row_top, strokeColor=AMBER, strokeWidth=1.5)) d.add(Line(arr1_x2, row_top, arr1_x2 - 7, row_top + 4, strokeColor=AMBER, strokeWidth=1.5)) d.add(Line(arr1_x2, row_top, arr1_x2 - 7, row_top - 4, strokeColor=AMBER, strokeWidth=1.5)) # ε₀ box (amber) d.add(Rect(end_bx, top_by, end_bw, bh, fillColor=AMBER_LITE, strokeColor=AMBER, strokeWidth=1.8, rx=3, ry=3)) d.add(String(end_bx + 10, top_by + bh - 13, 'ε', fontSize=12, fontName='DV-B', fillColor=AMBER)) d.add(String(end_bx + 20, top_by + bh - 17, '0', fontSize=8, fontName='DV-B', fillColor=AMBER)) d.add(String(end_bx + 5, top_by + 5, '(snap: c1)', fontSize=7.5, fontName='DV-I', fillColor=AMBER)) # Row label (above top row) d.add(String(x0, top_by + bh + 8, 'Ordinal: each stage strictly below ε-zero', fontSize=8, fontName='DV-I', fillColor=GREY_TEXT)) # ── 2-adic row (bottom, indigo) ─────────────────────────────────────────── for i, lbl in enumerate(stage_norm): bx = x0 + i * (bw + spacing) d.add(Rect(bx, bot_by, bw, bh, fillColor=INDIGO_LITE, strokeColor=INDIGO, strokeWidth=1.2, rx=3, ry=3)) lbl_x = bx + max(4, (bw - len(lbl) * 5.5) / 2) d.add(String(lbl_x, bot_by + bh - 13, lbl, fontSize=9, fontName='DV-B', fillColor=INDIGO)) if i < n - 1: d.add(Line(bx + bw + 2, row_bot, bx + bw + spacing - 2, row_bot, strokeColor=INDIGO, strokeWidth=1.0)) # 2-adic dots for j in range(3): d.add(Circle(dots_x + j * 8, row_bot, 2, fillColor=INDIGO, strokeColor=INDIGO, strokeWidth=0)) # Arrow to 0 = ⊥ box arr2_x1 = dots_x + 3 * 8 + 4 arr2_x2 = end_bx - 3 d.add(Line(arr2_x1, row_bot, arr2_x2, row_bot, strokeColor=INDIGO, strokeWidth=1.5)) d.add(Line(arr2_x2, row_bot, arr2_x2 - 7, row_bot + 4, strokeColor=INDIGO, strokeWidth=1.5)) d.add(Line(arr2_x2, row_bot, arr2_x2 - 7, row_bot - 4, strokeColor=INDIGO, strokeWidth=1.5)) # 0 = ⊥ box (indigo) d.add(Rect(end_bx, bot_by, end_bw, bh, fillColor=INDIGO_LITE, strokeColor=INDIGO, strokeWidth=1.8, rx=3, ry=3)) d.add(String(end_bx + 5, bot_by + bh - 13, '0 = ⊥', fontSize=9.5, fontName='DV-B', fillColor=INDIGO)) d.add(String(end_bx + 5, bot_by + 5, '(limit)', fontSize=7.5, fontName='DV-I', fillColor=INDIGO)) # Row label (above bottom row, in the inter-row gap) d.add(String(x0, bot_by + bh + 8, '2-adic norm of encoding (converges to 0 = ⊥):', fontSize=8, fontName='DV-I', fillColor=GREY_TEXT)) # ── Vertical dashed connectors between rows ─────────────────────────────── for i in range(n): bx_mid = x0 + i * (bw + spacing) + bw / 2 d.add(Line(bx_mid, top_by - 2, bx_mid, bot_by + bh + 2, strokeColor=colors.HexColor('#BBBBBB'), strokeWidth=0.8, strokeDashArray=[3, 3])) # End column connector bx_mid = end_bx + end_bw / 2 d.add(Line(bx_mid, top_by - 2, bx_mid, bot_by + bh + 2, strokeColor=colors.HexColor('#BBBBBB'), strokeWidth=0.8, strokeDashArray=[3, 3])) # Caption d.add(String(14, 10, 'Same tower, two perspectives. Teal (top): ordinal stages approach ε-zero. ' 'Indigo (bottom): their 2-adic norms approach 0.', fontSize=7.5, fontName='DV-I', fillColor=GREY_TEXT)) return d VERSION = '1.4' def build(): out_path = os.path.join(PROJECT_ROOT, 'ZP-L_Illustrated_Companion.pdf') def footer_cb(canvas, doc): canvas.saveState() canvas.setFont('DV-I', 8) canvas.setFillColor(colors.grey) canvas.drawCentredString( LETTER[0] / 2, 0.6 * inch, 'Zero Paradox ZP-L Companion | Incomputability Convergence | May 2026') canvas.restoreState() doc = SimpleDocTemplate( out_path, pagesize=LETTER, leftMargin=LM, rightMargin=RM, topMargin=TM, bottomMargin=BM, title='ZP-L Illustrated Companion', author='Zero Paradox Project', onFirstPage=footer_cb, onLaterPages=footer_cb) E = [] # ── Header banner ───────────────────────────────────────────────────────── hdr_ts = TableStyle([ ('BACKGROUND', (0, 0), (-1, -1), COMP_BLUE), ('TOPPADDING', (0, 0), (-1, -1), 8), ('BOTTOMPADDING', (0, 0), (-1, -1), 8), ('LEFTPADDING', (0, 0), (-1, -1), 10), ]) hdr = Table([[Paragraph('ZP-L Illustrated Companion', ParagraphStyle('hdr', fontName='DV-B', fontSize=11, textColor=WHITE))]], colWidths=[TW]) hdr.setStyle(hdr_ts) E.append(hdr) E.append(sp(6)) # ── Title block ─────────────────────────────────────────────────────────── E += [ Paragraph('The Ordinal Summit', CS['title']), Paragraph('Where the Tower Snaps to c₁', CS['subtitle']), Paragraph('ZP Companion | Version ' + VERSION + ' | May 2026', CS['meta']), Paragraph( 'This companion explains the ideas in plain language with diagrams and examples. ' 'It is not the formal document — every claim here restates a result already ' 'proved in ZP-L Incomputability Convergence. Consult that document for the ' 'authoritative mathematics.', CS['disc']), ] # ── What Is ZP-L Doing? ─────────────────────────────────────────────────── E.append(Paragraph('What Is ZP-L Doing?', CS['h1'])) E.append(cbody( 'ZP-K proved that the initial machine state c₀ is a Kleene fixed point: ' 'a program whose behavior is determined entirely by its own index, guaranteed to exist ' 'by the second recursion theorem. ZP-L picks up the thread from a different ' 'direction: the ordinal direction. If a map ϕ assigns machine phases to ordinals ' '— sending c₀ to everything below a certain point and c₁ above it ' '— what is that threshold ordinal? ZP-L establishes the answer: ε₀, ' 'the first fixed point of the map α ↦ ω^α.')) E.append(cbody( 'This is not an arbitrary choice. ZP-L proves that ε₀ is the minimal ' 'threshold — no monotone, tower-aligned map can snap before ε₀, and ' 'the canonical map snaps exactly there. ZP-L also establishes the connection to ' 'ZP-B: as the tower stages approach ε₀ in ordinal order, their ' '2-adic encodings converge to 0 = ⊥ in ℤ₂. The same sequence ' 'witnesses both convergences simultaneously.')) E.append(sp(4)) E.append(example_box('Real-world analogy — the unreachable horizon', [ 'Imagine a path where each step is longer than the last: you walk 1 mile, then ' '2, then 4, then 8, ... You are always getting further from the start, but you ' 'are also always somewhere on the path — never at the horizon. The horizon ' '(ε₀) is the limit of all those steps combined. It exists as a ' 'mathematical object, but no finite number of steps reaches it.', 'The ordinal tower works the same way. The snap that ZP-E proved occurs at ε₀ ' 'is not a step you can take from inside the tower. It is the point where the tower ' 'stops and something new begins.', ])) E.append(sp(8)) # ── What Is ε₀? ─────────────────────────────────────────────────────────── E.append(Paragraph('What Is ε₀?', CS['h1'])) E.append(cbody( 'ε₀ (epsilon-zero) is the smallest ordinal α satisfying the ' 'equation ω^α = α. In other words, it is the first fixed point ' 'of the map that sends any ordinal α to ω^α (omega raised to the ' 'power α). This is not a coincidence or a definition by fiat — it is ' 'a property ε₀ satisfies and no smaller ordinal does.')) E.append(cbody( 'The tower 0, 1, ω, ω^ω, ω^ω^ω, … climbs ' 'through the ordinals, each stage being ω raised to the previous stage. ' 'Every stage is strictly below ε₀, and ε₀ is their limit — ' 'the supremum of the whole sequence. It is never reached from below; it is ' 'the boundary above all stages.')) E.append(sp(4)) E.append(snap_tower_diagram()) E.append(ccaption( 'The tower stages 0, 1, ω, ω^ω, … all lie strictly below ε₀ ' 'and map to c₀. The snap transition to c₁ occurs at the threshold ε₀ itself. ' 'The arrow marks the snap. ZP-L §VII: epsilon_zero_snap_canonical.')) E.append(sp(4)) E.append(remember_box( 'Remember: ε₀ is not "infinity." It is a specific countable ordinal — ' 'the first one satisfying ω^α = α. Ordinals larger than ε₀ ' 'exist (ε₀ + 1, ε₁, and many more). ZP-L is not claiming that ' 'ε₀ is the largest ordinal or that the framework breaks down above it. It is ' 'the minimal snap threshold for monotone, tower-aligned maps — and that minimality ' 'is exactly what is proved.')) E.append(sp(8)) # ── Why ε₀ Is the Exact Threshold ──────────────────────────────────────── E.append(Paragraph('Why ε₀ Is the Exact Threshold', CS['h1'])) E.append(cbody( 'Two facts together pin ε₀ as the minimal snap threshold. They work like ' 'a lower bound and an upper bound that meet at the same point.')) E.append(cbody( 'Lower bound (snap cannot happen before ε₀): The fundamental sequence ' 'is cofinal in ε₀. This means: for any ordinal α below ε₀, ' 'some tower stage eventually exceeds α. A monotone map that assigns c₀ ' 'to every tower stage must therefore assign c₀ to α too (it cannot ' 'increase between a stage above α and α itself). So no ordinal strictly ' 'below ε₀ can be a snap point for such a map.')) E.append(cbody( 'Upper bound (snap does happen at ε₀): ε₀ is itself a ' 'fixed point of ω^· (ω^ε₀ = ε₀). A map that ' 'assigns c₁ to all fixed points of ω^· must assign c₁ to ε₀. ' 'Together with the lower bound, ε₀ is the first place where c₁ can ' 'and must appear.')) E.append(cbody( 'The canonical witness map ϕ(α) = c₀ if α < ε₀, ' 'else c₁ satisfies all five conditions at once — monotonicity, ' 'tower-alignment, fixed-point-respecting, snapping at ε₀, and minimality ' '— with no free hypotheses. This is the central result of ZP-L.')) E.append(sp(4)) E.append(remember_box( '"Minimal" does not mean "unique." ZP-L proves that no snap can occur strictly ' 'before ε₀ (under the stated conditions), not that ε₀ is the ' 'only possible snap point. Maps that also assign c₁ to ordinals above ε₀ ' 'are not ruled out. The framework fixes ε₀ as the threshold by ' 'the canonical witness, not by uniqueness of all satisfying maps.')) E.append(sp(8)) # ── The Two-Adic Connection ─────────────────────────────────────────────── E.append(Paragraph('The Two-Adic Connection', CS['h1'])) E.append(cbody( 'ZP-B established that 0 = ⊥ in the 2-adic integers ℤ₂ is the ' 'valuative sink: the 2-adic valuation of 0 is infinite, which means 0 sits at the ' 'bottom of the 2-adic metric. ZP-L connects this to the ordinal tower via an ' 'encoding of ordinals below ε₀ into ℤ₂ using their Cantor ' 'normal forms.')) E.append(cbody( 'The encoding (cnfToZp2 in ZPL.lean) maps the n-th tower stage to 2n ' 'in ℤ₂. The 2-adic norm of 2n is (1/2)n, which ' 'goes to 0 as n increases. So as the ordinal tower climbs toward ε₀ from ' 'below, its 2-adic image converges to 0 = ⊥ in the 2-adic metric ' '(the norms (1/2)n decrease monotonically and converge to 0). Two convergences, ' 'one tower.')) E.append(sp(4)) E.append(dual_convergence_diagram()) E.append(ccaption( 'Same tower stages, two perspectives. Teal (top row): ordinal stages 1, ω, ω^ω, … ' 'approach ε₀ from below. Indigo (bottom row): the 2-adic norms of their ' 'encodings 1/2, 1/4, 1/8, … converge to 0 = ⊥. ' 'ZP-L §VII: snap_zp2_correspondence.')) E.append(sp(4)) E.append(cbody( 'This dual convergence is what snap_zp2_correspondence formalizes in ZP-L §VII: ' 'four jointly established facts about the same tower sequence — ' 'all stages below ε₀ in ordinal order, all assigned c₀ by the ' 'canonical map, all encoding to 2n in ℤ₂ with 2-adic norm ' '(1/2)n → 0, and the canonical map snapping to c₁ at ε₀.')) E.append(sp(8)) # ── The Kleene Connection ───────────────────────────────────────────────── E.append(Paragraph('The Kleene Connection', CS['h1'])) E.append(cbody( 'ZP-K identified ⊥ as a Kleene fixed point: a program that is its own output, ' 'guaranteed to exist by Kleene\'s second recursion theorem. ZP-L identifies ' 'ε₀ as an ordinal fixed point: the first ordinal satisfying ω^α = α, ' 'guaranteed to exist by the fixed-point theorem for normal functions. Both fixed-point ' 'proofs require Classical.choice in their Lean formalizations. In each case, the choice ' 'axiom enters at a non-constructive selection step: the ordinal proof uses it for the ' 'supremum that defines ε₀; the Kleene proof uses it for the fixed-point ' 'selection. Whether these reflect the same underlying mathematical phenomenon — ' 'or are coincidentally parallel — is the open question ZPL.lean §I poses.')) E.append(cbody( 'ZP-L §VI (kleene_ordinal_snap_bridge) names this structural parallel explicitly. ' 'The theorem itself is purely ordinal — no Code or eval object appears in it. ' 'What the section establishes is that the hypothesis structure of the two proofs ' 'is the same: diagonalization, non-constructive selection, fixed-point existence.')) E.append(sp(4)) E.append(example_box('Two rooms, same pattern', [ 'Imagine two mathematicians working in separate rooms. One (ZP-K) is computing ' 'with programs and asking: what program runs itself? The other (ZP-L) is computing ' 'with ordinals and asking: what ordinal satisfies ω^α = α? Neither ' 'knows what the other is doing. When they compare notes, they find the same proof ' 'structure: the same diagonal argument, the same non-constructive selection step, ' 'the same kind of fixed-point existence result.', 'ZPM formalizes this parallel with a type bridge between the two settings. ' 'The two rooms share the same floor plan.', ])) E.append(sp(8)) # ── Proof-Theoretic Connection ──────────────────────────────────────────── E.append(Paragraph('Convergence with Proof Theory', CS['h1'])) E.append(cbody( 'ZP-L derives ε₀ as the snap threshold from ordinal fixed-point structure ' 'alone — ω-tower iteration, the fixed-point property of ' 'α ↦ ω^α, and Cantor normal form encodings into ℤ₂. ' 'Remark R-L.1 in the formal document notes a structural alignment with an independent ' 'result from proof theory.')) E.append(cbody( 'Gentzen (1936) proved that ε₀ is the proof-theoretic ordinal of Peano ' 'Arithmetic: PA can prove transfinite induction up to any ordinal strictly below ' 'ε₀, but not for ε₀ itself. ε₀ is the exact ordinal ' 'boundary of PA’s own proof machinery — the furthest point its provability ' 'reaches before requiring a strictly stronger system.')) E.append(cbody( 'ZP-L and Gentzen arrive at ε₀ from entirely separate starting points. ' 'ZP-L starts from ordinal fixed-point structure: ε₀ is where ω-tower ' 'self-iteration closes on itself. Gentzen starts from proof theory: ε₀ is ' 'where PA’s provability tower runs out. Neither derivation references the ' 'other’s domain. Both locate the same boundary.')) E.append(cbody( 'The convergence is notable. ZP-L’s fixed-point derivation and Gentzen’s ' 'proof-theoretic analysis were conducted in separate domains with separate machinery. ' 'That both locate ε₀ is a structural observation, not an argument for ' 'either result. Both stand or fall on their own proofs.')) E.append(sp(4)) E.append(remember_box( 'ZP does not prove any part of Gödel’s incompleteness theorems, and does ' 'not reprove Gentzen’s ordinal analysis of PA. The connection is a structural ' 'observation: two independent formal derivations arrive at the same ordinal boundary. ' 'Gentzen (1936) established that ε₀ is the specific ordinal where ' 'PA’s proof-theoretic strength is exhausted. ZP-L established ε₀ as ' 'the snap threshold from ordinal fixed-point structure. No formal equivalence ' 'between the two derivations is claimed.')) E.append(sp(8)) # ── Axiom Footprint Note ────────────────────────────────────────────────── E.append(Paragraph('A Note on Classical.choice', CS['h1'])) E.append(cbody( 'Every ZP-L theorem carries the axiom footprint [propext, Classical.choice, ' 'Quot.sound]. This is the standard footprint of Lean 4 + Mathlib for any theorem ' 'that uses ordinal theory, p-adic analysis, or computability. It is not a novel ' 'ZP-L commitment.')) E.append(cbody( 'What is notable is where Classical.choice appears. Across the four mathematical ' 'settings of the ZP framework — topology (ZP-B), information theory (ZP-C), ' 'set theory and computation (ZP-J/K), and ordinal theory (ZP-L) — the same ' 'axiom appears at the same structural step: the non-constructive diagonal. ' 'ZP-L §I documents this convergence. Whether Classical.choice is structurally ' 'forced by the ZP framework — rather than merely inherited from Mathlib ' 'infrastructure — remains an open question.')) E.append(sp(8)) # ── Key Result ──────────────────────────────────────────────────────────── E.append(key_result_box( 'Key Result — ZP-L: The Ordinal Snap Threshold', 'epsilon_zero_snap_canonical (ZPL.lean §VII): The canonical map ' 'ϕ(α) = c₀ if α < ε₀, else c₁ ' 'satisfies all five conditions simultaneously — monotone, tower-aligned ' '(c₀ on every fundamental sequence stage), fixed-point-respecting ' '(c₁ on every fixed point of ω^·), snapping at ε₀, ' 'and ε₀ minimal — with no free hypotheses. ' 'snap_zp2_correspondence co-proves that the same tower witnesses both the ' 'ordinal approach to ε₀ and the 2-adic convergence to 0 = ⊥. ' 'All theorems proved without sorry. ZPM formalizes the type bridge between the ' 'ordinal and machine-phase encodings. ✓')) print(f'Building: {out_path}') doc.build(E) print(f'Done. File size: {os.path.getsize(out_path) // 1024} KB') if __name__ == '__main__': build()