"""
Zero Paradox — ZP-M: Kleene-Ordinal Bridge PDF Builder
Version 1.0 | May 2026
v1.0: Initial release. All theorems §I–§IV proved sorry-free in Lean 4.
Axiom footprint: [propext, Classical.choice, Quot.sound] throughout.
Closes the two gaps left by ZP-K (hfp free hypothesis) and ZP-L (type bridge).
Follows all rules in scripts/PDF_Rendering_Standards.md.
"""
import os
from zp_utils import *
VERSION = '1.0'
def build():
out_path = os.path.join(PROJECT_ROOT, 'ZP-M_Kleene_Ordinal_Bridge.pdf')
print(f'[build_zpm] Output: {out_path}')
doc = make_doc(out_path, 'ZP-M: Kleene-Ordinal Bridge',
'ZP-M: Kleene-Ordinal Bridge', 'Version ' + VERSION)
E = []
print('[build_zpm] Building title block...')
E += [
sp(12),
Paragraph('THE ZERO PARADOX', S['title']),
Paragraph('ZP-M: Kleene–Ordinal Bridge', S['title']),
Paragraph('Version ' + VERSION + ' | May 2026', S['subtitle']),
Paragraph(
'v1.0: Initial release. '
'All theorems §I–§IV proved sorry-free in Lean 4. '
'Closes the hfp free hypothesis (ZP-L) and the snapEmbed type bridge. '
'Axiom footprint: [propext, Classical.choice, Quot.sound] throughout.',
S['note']),
sp(10),
hr(),
sp(4),
]
E.append(body(
'ZP-M bridges the two prior layers — ZP-K (computational grounding via Kleene\'s '
'second recursion theorem) and ZP-L (ordinal snap threshold at ε₀) — '
'with two formal results. First, the free hypothesis hfp in '
'snap_exactly_at_epsilon_zero (ZP-L §VI) is proved to follow from a minimal '
'alignment hypothesis plus monotonicity: hfp is not an independent condition. '
'Second, the canonical type bridge snapEmbed : MachinePhase → ℤ₂ '
'formalizes the structural triangle connecting the pre-snap state c₀ '
'(Kleene quine, ZP-K), the ordinal snap at ε₀ (ZP-L), and the '
'2-adic limit 0 (ZP-B).'))
E.append(body(
'The closing result (§IV) records that both the Kleene recursion theorem and '
'the ordinal fixed-point ε₀ = ω^ε₀ are instances of '
'the same diagonalization pattern: a self-referential operation produces a forced '
'fixed point. The two domains — computability theory (codes and Gödel numbers) '
'and ordinal theory (ω-tower iteration) — use no shared mathematical machinery, '
'but the structural schema is identical. Remark R-M.1 tracks what this means for '
'DA-1 Path 2 and the boundary of the diagonalization frame.'))
E.append(hr())
# ── Section I: The snapEmbed Morphism ──────────────────────────────────────
print('[build_zpm] Building Section I...')
E += [
Paragraph('Section I: The snapEmbed Morphism', S['h1']),
hr(),
]
E.append(body(
'snapEmbed is the canonical type bridge from ZP-E\'s machine-phase state space '
'to ZP-B\'s 2-adic integers. The pre-snap state c₀ maps to 1 (a 2-adic unit); '
'the snap state c₁ maps to 0 (the 2-adic limit of the tower encodings). '
'Under multiplication on ℤ₂, 0 is absorbing — mirroring exactly the '
'join structure on MachinePhase, where c₁ is the absorbing element.'))
E.append(body(
'Within the ZP framework, 0 ∈ ℤ₂ plays the role of ⊥ — '
'it is the 2-adic valuation limit and the fixed point of multiplication by 2. '
'snapEmbed makes this modelling commitment concrete: c₁ maps to 0 because '
'c₁ IS the object at infinite 2-adic depth. This is a modelling commitment, '
'not a ring-theoretic theorem.'))
E.append(def_box(
'Definition: snapEmbed (ZPM.lean §I)',
[
'snapEmbed : MachinePhase → ℤ₂',
' snapEmbed c₀ = 1 (pre-snap: 2-adic unit)',
' snapEmbed c₁ = 0 (snap state: 2-adic zero = 2-adic limit of tower)',
'',
'The morphism property: join on MachinePhase (c₁ is absorbing under join) '
'corresponds to multiplication on ℤ₂ (0 is absorbing under ×). '
'Both structures share the absorbing-element pattern — the bridge is structural, '
'not incidental.',
]
))
E.append(sp(6))
E.append(result_box(
'Theorem: snapEmbed_injective (ZPM.lean §I)',
[
'Function.Injective snapEmbed',
'c₀ and c₁ map to distinct 2-adic integers (1 ≠ 0 in ℤ₂).',
'Proof: case split on MachinePhase; simp_all closes each case.',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(4))
E.append(result_box(
'Theorem: snapEmbed_mul_morphism (ZPM.lean §I)',
[
'∀ a b : MachinePhase, snapEmbed (join a b) = snapEmbed a × snapEmbed b',
'snapEmbed sends the join operation to multiplication.',
'Under this map, the absorbing-element structure is preserved:',
' join c₁ x = c₁ for all x ↔ 0 × y = 0 for all y ∈ ℤ₂.',
'Proof: case split; simp [snapEmbed].',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(4))
E.append(result_box(
'Lemma: snapEmbed_c0_val (ZPM.lean §I)',
[
'(snapEmbed c₀).valuation = 0',
'c₀ maps to a 2-adic unit: valuation 0, norm 1.',
'Proof: simp via PadicInt.valuation_one.',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(4))
E.append(result_box(
'Lemma: snapEmbed_c1_dvd (ZPM.lean §I)',
[
'∀ n : ℕ, (2 : ℤ₂)^n ∣ snapEmbed c₁',
'c₁ maps to 0, which is divisible by all powers of 2.',
'0 ∈ ℤ₂ is divisible by 2^n for every n — infinite 2-adic depth.',
'This is the formal signature of ⊥ = {⊥}: infinite 2-adic valuation.',
'Proof: simp [snapEmbed_c1].',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(6))
E.append(remark_box(
'Remark: snapEmbed vs the Identification Conjecture',
[
'snapEmbed establishes the morphism property (join ↦ ×) and the '
'absorbing-element correspondence. It does not derive the identification '
'ε₀ ↔ ⊥ as a type-theoretic theorem: establishing '
'that snap_exactly_at_epsilon_zero\'s threshold IS 0 ∈ ℤ₂ '
'via an order-preserving embedding would require ZPSemilattice morphisms '
'between Ordinal and MachinePhase, which are not defined in this library.',
'What the bridge achieves: c₁ (the snap state assigned at ε₀) '
'maps to 0 (the 2-adic limit) under snapEmbed. The triangle is formally exhibited. '
'The conjectured stronger bridge — Classical.choice forced by ZP metric '
'collapse — is deferred to §V (future work).',
]
))
E.append(sp(6))
# ── Section II: Closing the hfp Gap ────────────────────────────────────────
print('[build_zpm] Building Section II...')
E += [
hr(),
Paragraph('Section II: Closing the hfp Gap', S['h1']),
hr(),
]
E.append(body(
'snap_exactly_at_epsilon_zero (ZP-L §VI) carries a free hypothesis hfp asserting '
'that for any map ϕ : Ordinal → MachinePhase, every fixed point of '
'ω^· maps to c₁. This hypothesis is required for the upper-bound '
'direction of the minimality argument (ε₀ is the first snap point). '
'The canonical witness in epsilon_zero_snap_canonical (ZP-L §VII) satisfies hfp '
'directly by case analysis, but hfp is not derived from the structural axioms.'))
E.append(body(
'ZP-M §II closes this gap. Given monotonicity and ϕ ε₀ = c₁ '
'as a minimal alignment hypothesis, hfp follows. The argument: for any fixed point '
'α of ω^·, epsilonZero_le_fixedPoint gives ε₀ ≤ α; '
'monotonicity then chains ϕ ε₀ ≤ ϕ α; substituting '
'c₁ and using c₁\'s absorbing property gives ϕ α = c₁.'))
E.append(result_box(
'Theorem: hfp_from_epsilon_zero (ZPM.lean §II)',
[
'For any ϕ : Ordinal → MachinePhase satisfying:',
' hmono: ∀ α ≤ β, join (ϕ α) (ϕ β) = ϕ β',
' hε₀: ϕ epsilonZero = c₁',
'we have: ∀ α, ω^α = α → ϕ α = c₁.',
'',
'Proof: epsilonZero_le_fixedPoint gives ε₀ ≤ α; '
'hmono gives join c₁ (ϕ α) = ϕ α; '
'join c₁ x = c₁ for all x (absorbing property of c₁), '
'so c₁ = ϕ α.',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(4))
E.append(result_box(
'Theorem: snap_unconditional (ZPM.lean §II)',
[
'For any ϕ satisfying hmono, h0 (tower stages ↦ c₀), '
'and hε₀ (ϕ ε₀ = c₁):',
' ϕ ε₀ = c₁ ∧ '
'∀ α, ϕ α = c₁ → ε₀ ≤ α.',
'ε₀ is the minimal snap threshold under minimal hypotheses.',
'Proof: snap_exactly_at_epsilon_zero with hfp supplied by hfp_from_epsilon_zero.',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(6))
E.append(callout(
'What §II achieves: hfp is no longer a free hypothesis in the minimality theorem. '
'Given ϕ ε₀ = c₁ (the alignment condition: the map snaps at '
'ε₀) plus monotonicity, the full minimality result follows from the ordinal '
'structure alone. hfp is a derived consequence, not an additional commitment.',
bg=GREEN_LITE, border=GREEN
))
E.append(sp(6))
# ── Section III: The Kleene-Ordinal Triangle ────────────────────────────────
print('[build_zpm] Building Section III...')
E += [
hr(),
Paragraph('Section III: The Kleene–Ordinal Triangle', S['h1']),
hr(),
]
E.append(body(
'ZP-K established: c₀ = ⊥ is a Quine atom '
'(da1_closed_concrete : IsQuineAtom (⊥ : MachinePhase)). '
'ZP-L established: the canonical snap map assigns c₁ exactly at ε₀, '
'with tower encodings in ℤ₂ converging to 0. '
'The triangle connects all three objects formally:'))
E.append(data_table(
headers=['Edge', 'Objects connected', 'Formal content'],
rows_data=[
['A ↔ C (ordinal snap)',
'ε₀ ↔ c₁',
'Canonical snap map: stages below ε₀ ↦ c₀; '
'ε₀ ↦ c₁ (ZP-L §VII)'],
['A ↔ B (2-adic convergence)',
'Tower → 0 ∈ ℤ₂',
'cnfToZp2(towerNONote n) → 0 in ℤ₂ (ZP-L §IV)'],
['B ↔ C (type bridge)',
'c₁ ↔ 0 ∈ ℤ₂',
'snapEmbed c₁ = 0 (§I above)'],
],
col_widths=[TW * 0.20, TW * 0.22, TW * 0.58],
))
E.append(sp(6))
E.append(result_box(
'Theorem: snap_state_zp2_is_zero (ZPM.lean §III)',
[
'snapEmbed ((λ α : Ordinal, if α < ε₀ then c₀ else c₁) '
'ε₀) = 0',
'The canonical snap map assigns c₁ at ε₀; snapEmbed sends c₁ to 0.',
'The snap state at the ordinal threshold maps to the 2-adic zero.',
'Proof: simp (the if-condition evaluates to False at α = ε₀).',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(4))
E.append(result_box(
'Theorem: zpm_triangle (ZPM.lean §III)',
[
'All three edges of the triangle, co-proved:',
'(A ↔ C) ∀ n : ℕ, fundamentalSeq n < ε₀',
'(A ↔ C) (λ α, if α < ε₀ then c₀ else c₁) '
'ε₀ = c₁',
'(A ↔ B) Filter.Tendsto (λ n, cnfToZp2 (towerNONote n)) '
'Filter.atTop (nhds 0)',
'(B ↔ C) snapEmbed (λ α, if α < ε₀ then c₀ '
'else c₁) ε₀ = 0',
'Proof: ⟨epsilonZero_tower_lt, if_neg (lt_irrefl ε₀), '
'tower_converges_to_zero, snap_state_zp2_is_zero⟩.',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(6))
# ── Section IV: Shared Diagonalization Pattern ─────────────────────────────
print('[build_zpm] Building Section IV...')
E += [
hr(),
Paragraph('Section IV: Shared Diagonalization Pattern', S['h1']),
hr(),
]
E.append(body(
'Both the Kleene recursion theorem (ZP-K) and the ordinal fixed-point ε₀ '
'(ZP-L) arise from the same structural schema: a self-referential operation has a '
'forced fixed point. In computability theory, the diagonal applies to codes and '
'their Gödel numbers. In ordinal theory, the diagonal applies to the tower iteration '
'α ↦ ω^α. The two domains share no mathematical machinery, '
'but the diagonalization pattern is identical.'))
E.append(data_table(
headers=['Domain', 'Self-referential operation', 'Forced fixed point'],
rows_data=[
['Computability (ZP-K)',
'eval c = selfApply c (c runs on its own Gödel number)',
'∃ c : Code, IsComputationalQuine c'],
['Ordinal theory (ZP-L)',
'ω^α = α (α is a fixed point of ω-exponentiation)',
'ε₀ = nfp (ω^·) 0, the least such α'],
],
col_widths=[TW * 0.23, TW * 0.42, TW * 0.35],
))
E.append(sp(6))
E.append(result_box(
'Theorem: both_fixed_points_exist (ZPM.lean §IV)',
[
'(∃ c : Code, ∀ n, eval c n = eval c (encode c + n)) ∧',
'(∃ α : Ordinal, ω^α = α ∧ '
'∀ β, ω^β = β → α ≤ β)',
'Both diagonalization patterns produce fixed points, co-proved in one formal context.',
'Left: Kleene quine (period = Gödel number of c), via computational_quine_exists.',
'Right: ε₀ = ω^ε₀, minimal; via epsilonZero_fixedPoint '
'and epsilonZero_le_fixedPoint.',
'The co-existence is the formal content: two forced fixed points, two domains, '
'one theorem.',
'Lean purity: [propext, Classical.choice, Quot.sound]. ✓',
]
))
E.append(sp(6))
E.append(remark_box(
'Remark R-M.1: DA-1 Path 2 and the Limits of the Diagonalization Frame',
[
'both_fixed_points_exist establishes that Kleene diagonalization (a code on '
'its own Gödel number) and ordinal diagonalization (ε₀ = ω^ε₀, '
'least fixed point) are the same structural pattern in two domains. Both are '
'textbook instances of the diagonalization schema.',
'L-INF (ZP-C §II: ⊥ has divergent surprisal — unbounded information content, '
'incompressible by any finite description) is structurally analogous. Whether it '
'fits the same diagonalization schema formally is the open question.',
'The formally unconnected instance is L-INF. This gap is DA-1 Path 2 — the '
'informational bridge. The reason Path 2 resisted formalization is now visible '
'from this layer: L-INF is a measure-theoretic statement (Shannon entropy, '
'probability distributions) while the Kleene quine is a computability-theoretic '
'statement (partial recursive functions, Gödel encoding). The two frameworks '
'share no mathematical machinery.',
'The diagonalization frame established here provides the common conceptual ground, '
'but the formal bridge requires the Kolmogorov complexity connection: '
'incompressibility is the concept that lives in both worlds simultaneously. '
'That bridge is outside the current Lean scope, pending AIT infrastructure '
'not yet in Mathlib.',
'DA-1 Path 2 was recharacterized in ZP-E/ZP-K as a foundational commitment '
'rather than a missing proof. The diagonalization frame here makes the boundary '
'precise: the gap is not a skipped proof step but a genuine framework separation — '
'measure-theoretic surprisal on one side, computability-theoretic encoding on the '
'other, with no shared machinery in current Mathlib.',
]
))
E.append(sp(6))
# ── Theorem Table ───────────────────────────────────────────────────────────
print('[build_zpm] Building theorem table...')
E += [
hr(),
Paragraph('Theorem Summary', S['h1']),
hr(),
]
E.append(data_table(
headers=['Theorem', 'Section', 'Status'],
rows_data=[
['snapEmbed_injective', '§I', 'Proved ✓'],
['snapEmbed_mul_morphism', '§I', 'Proved ✓'],
['snapEmbed_c0_val', '§I', 'Proved ✓'],
['snapEmbed_c1_dvd', '§I', 'Proved ✓'],
['hfp_from_epsilon_zero', '§II', 'Proved ✓'],
['snap_unconditional', '§II', 'Proved ✓'],
['snap_state_zp2_is_zero', '§III', 'Proved ✓'],
['zpm_triangle', '§III', 'Proved ✓'],
['both_fixed_points_exist', '§IV', 'Proved ✓'],
],
col_widths=[TW * 0.55, TW * 0.15, TW * 0.30],
))
E.append(sp(4))
E.append(axiom_box(
'Axiom Purity',
[
'All theorems carry axiom footprint: [propext, Classical.choice, Quot.sound].',
'These are standard Mathlib infrastructure axioms, inherited from ordinal theory '
'(ZP-L), 2-adic analysis (ZP-B), and computability theory (ZP-K).',
'Classical.choice is load-bearing in both the computability fixed-point '
'(Kleene\'s theorem) and the ordinal fixed-point (nfp). Its presence is '
'expected and documented.',
'Zero sorry in ZPM.lean. Verified: lake build, May 2026.',
]
))
E.append(sp(6))
E += [
hr(),
Paragraph(
'End of ZP-M v1.0 | Kleene–Ordinal Bridge | '
'snapEmbed type bridge | hfp gap closed | zpm_triangle co-proved | '
'both_fixed_points_exist | R-M.1: DA-1 Path 2 boundary | '
'All ZPM.lean theorems verified. Axioms: [propext, Classical.choice, Quot.sound].',
S['endnote']),
]
print('[build_zpm] Building document...')
doc.build(E)
print(f'[build_zpm] Done: {out_path}')
if __name__ == '__main__':
build()