"""
Build ZP-E Illustrated Companion
Version 1.11 | May 2026
v1.11: Add Goodstein/proof-theoretic context for ε₀ in Four Descriptions section.
v1.10: Strip version number from companion footer.
v1.9: Strip version numbers from DA-1 historical narrative in body prose.
v1.7: Title "AX-1 becomes a theorem" → "the main causality axiom becomes a theorem"; remember
box 1 "emergence of any state from a null condition" → scoped to ⊥→ε₀ transition; remember
box 2 "universal ontology of state emergence" removed — replaced with scoped no-claims statement.
v1.6: Disclaimer updated — "formal ontology" replaced with "formal document"; "proven" → "proved".
v1.5: four_framework_diagram: "0 is isolated" label in ZP-B box replaced with "Clopen structure".
v1.4: "topological isolation" in the closing remember box replaced with "clopen separation" —
consistent with ZP-B/D fixes; "topological isolation" evokes isolated-point topology, which is
incorrect for 0 in Q2. The correct structural property is clopen-ball separation.
v1.3: DA-1 formally closed via ZP-K noted — Paths 1 and 3 now IN LEAN SCOPE;
da1_closed_concrete : IsQuineAtom(⊥ : MachinePhase) proved in Lean 4. Formal doc at v3.7.
v1.2: AIT bridge added as third DA-1 motivating path; DP-2 two-layer structure explained;
da1_minimal_path Lean verification noted. Formal doc at v3.0.
v1.1: DA-1 diagram label updated (no longer D7-based); DA-1 status clarified as Derived Proposition
grounded in ZP-A CC-2 (⊥ = {⊥}), not a freestanding design commitment.
"""

import os
from zp_utils import *
from reportlab.graphics.shapes import Drawing, Line, String, Rect
from reportlab.graphics import renderPDF

def four_framework_diagram():
    """Central 'Binary Snap' circle with four framework boxes pointing inward."""
    dw, dh = TW, 3.4 * inch
    d = Drawing(dw, dh)

    cx, cy = dw / 2, dh / 2

    # Central amber circle
    cr = 42
    from reportlab.graphics.shapes import Circle
    d.add(Circle(cx, cy, cr, fillColor=COMP_AMBER, strokeColor=COMP_AMBER, strokeWidth=0))
    d.add(String(cx - 26, cy + 6,  'Binary', fontSize=9.5, fontName='DV-B', fillColor=WHITE))
    d.add(String(cx - 17, cy - 7, 'Snap',   fontSize=9.5, fontName='DV-B', fillColor=WHITE))

    # Helper: draw a teal box with two text lines and an arrow toward the center
    def framework_box(bx, by, bw, bh, label, sub1, sub2, ax1, ay1, ax2, ay2):
        d.add(Rect(bx, by, bw, bh, fillColor=COMP_BLUE, strokeColor=COMP_BLUE,
                   strokeWidth=1, rx=4, ry=4))
        d.add(String(bx + 8, by + bh - 16, label, fontSize=9.5,
                     fontName='DV-B', fillColor=WHITE))
        d.add(String(bx + 8, by + bh - 28, sub1, fontSize=7.5,
                     fontName='DV-I', fillColor=colors.white))
        d.add(String(bx + 8, by + bh - 39, sub2, fontSize=7.5,
                     fontName='DV-I', fillColor=colors.white))
        # Arrow
        d.add(Line(ax1, ay1, ax2, ay2, strokeColor=COMP_BLUE, strokeWidth=1.8))
        dx, dy = ax2 - ax1, ay2 - ay1
        ln = (dx*dx + dy*dy) ** 0.5
        if ln > 0:
            ux, uy = dx/ln, dy/ln
            px, py = -uy, ux
            hs = 6
            d.add(Line(ax2, ay2,
                       ax2 - hs*ux + hs*0.5*px, ay2 - hs*uy + hs*0.5*py,
                       strokeColor=COMP_BLUE, strokeWidth=1.8))
            d.add(Line(ax2, ay2,
                       ax2 - hs*ux - hs*0.5*px, ay2 - hs*uy - hs*0.5*py,
                       strokeColor=COMP_BLUE, strokeWidth=1.8))

    bw, bh = 1.35*inch, 0.62*inch

    # Top: ZP-A (above)
    bx = cx - bw/2; by = cy + cr + 14
    framework_box(bx, by, bw, bh,
                  'ZP-A: Algebra', '⊥ ≤ x for all x', 'Join accumulates',
                  cx, by, cx, cy + cr + 2)

    # Bottom: ZP-C (below)
    by2 = cy - cr - 14 - bh
    framework_box(cx - bw/2, by2, bw, bh,
                  'ZP-C: Info Theory', 'I(x) → ∞ as x → 0', 'Singularity',
                  cx, by2 + bh, cx, cy - cr - 2)

    # Left: ZP-B
    bxl = cx - cr - 16 - bw; byl = cy - bh/2
    framework_box(bxl, byl, bw, bh,
                  'ZP-B: Topology', 'Clopen structure', 'No path returns',
                  bxl + bw, cy, cx - cr - 2, cy)

    # Right: ZP-D
    bxr = cx + cr + 16; byr = cy - bh/2
    framework_box(bxr, byr, bw, bh,
                  'ZP-D: Hilbert', 'T(0) = e₀', 'Orthogonal shift',
                  bxr, cy, cx + cr + 2, cy)

    d.add(String(14, 10,
                 'The Binary Snap (amber) described simultaneously in all four frameworks. '
                 'Each arrow is an independent mathematical description of the same event.',
                 fontSize=7.5, fontName='DV-I', fillColor=GREY_TEXT))
    return d

def tsnap_chain_diagram():
    """P₀ → DA-1 → L-RUN → TQ-IH → ZP-A D2 → T-SNAP derivation chain."""
    dw, dh = TW, 1.6 * inch
    d = Drawing(dw, dh)

    steps = [
        ('P₀',      'Incomp.\nthreshold'),
        ('DA-1',    '⊥={⊥}: no\nextl. interp.'),
        ('L-RUN',   'Exec =\nnon-null'),
        ('TQ-IH',   'No null-only\ntrace'),
        ('ZP-A D2', 'State change\n= Snap'),
        ('T-SNAP',  'Derived\ntheorem'),
    ]
    n = len(steps)
    bw = (dw - 0.3*inch) / n - 6
    bh = 0.52 * inch
    by = dh * 0.52
    gap = 6
    x0 = 10

    for i, (label, sub) in enumerate(steps):
        bx = x0 + i * (bw + gap)
        fill = COMP_AMBER if i == n-1 else COMP_BLUE
        d.add(Rect(bx, by, bw, bh, fillColor=fill, strokeColor=COMP_BLUE,
                   strokeWidth=0.8, rx=3, ry=3))
        lw = len(label) * 6.2
        d.add(String(bx + bw/2 - lw/2, by + bh - 16, label,
                     fontSize=9, fontName='DV-B', fillColor=WHITE))
        # Sub-label lines
        sub_lines = sub.split('\n')
        sub_y = by - 14
        for sl in sub_lines:
            sw = len(sl) * 5.2
            d.add(String(bx + bw/2 - sw/2, sub_y, sl,
                         fontSize=7, fontName='DV-I', fillColor=GREY_TEXT))
            sub_y -= 10

        if i < n-1:
            nx = bx + bw + gap
            ax1, ax2 = bx + bw + 1, nx - 1
            amid = by + bh/2
            d.add(Line(ax1, amid, ax2, amid, strokeColor=COMP_BLUE, strokeWidth=1.5))
            d.add(Line(ax2-5, amid-3, ax2, amid, strokeColor=COMP_BLUE, strokeWidth=1.5))
            d.add(Line(ax2-5, amid+3, ax2, amid, strokeColor=COMP_BLUE, strokeWidth=1.5))

    d.add(String(14, dh - 14,
                 'AX-1 (Binary Snap Causality) is now Theorem T-SNAP — derived, not assumed.',
                 fontSize=8, fontName='DV-B', fillColor=COMP_AMBER))
    return d

def axioms_table():
    """AX-B1 / AX-G1 / AX-G2 table."""
    hdr = [Paragraph('Commitment', CS['tbl_hdr']),
           Paragraph('Statement', CS['tbl_hdr'])]
    rows = [
        ['AX-B1',
         'Binary Existence. A state either exists or it does not. No third option. '
         'Directly verifiable by computation — not a novel commitment.'],
        ['AX-G1',
         'Initial Object Exists. There is a starting point that reaches everything. '
         'Not a novel commitment — grounded in ⊥ as the bottom element of the ZP-A semilattice.'],
        ['AX-G2',
         'Source Asymmetry. Nothing returns to the initial object. '
         'The origin is unreachable from outside. '
         'Not a novel commitment — follows from ZP-A antisymmetry and ZP-B C3.'],
    ]
    data = [hdr] + [[Paragraph(fix(r[0]), CS['tbl_cell']),
                     Paragraph(fix(r[1]), CS['tbl_cell'])] for r in rows]
    ts = TableStyle([
        ('BACKGROUND',    (0,0),(-1,0),  COMP_BLUE),
        ('ROWBACKGROUNDS',(0,1),(-1,-1), [WHITE, colors.HexColor('#F0F8F8')]),
        ('BOX',           (0,0),(-1,-1), 0.5, COMP_BLUE),
        ('LINEBELOW',     (0,0),(-1,0),  0.5, COMP_BLUE),
        ('INNERGRID',     (0,1),(-1,-1), 0.3, colors.HexColor('#CCCCCC')),
        ('TOPPADDING',    (0,0),(-1,-1), 5), ('BOTTOMPADDING',(0,0),(-1,-1), 5),
        ('LEFTPADDING',   (0,0),(-1,-1), 7), ('RIGHTPADDING', (0,0),(-1,-1), 7),
        ('VALIGN',        (0,0),(-1,-1), 'TOP'),
    ])
    t = Table(data, colWidths=[TW*0.18, TW*0.82])
    t.setStyle(ts); return t

VERSION = '1.11'


def build():
    out_path = os.path.join(PROJECT_ROOT,
                            'ZP-E_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-E Companion  |  Bridge Document  |  April 2026')
        canvas.restoreState()

    doc = SimpleDocTemplate(out_path, pagesize=LETTER,
                            leftMargin=LM, rightMargin=RM, topMargin=TM, bottomMargin=BM,
                            title='ZP-E 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-E Illustrated Companion',
                            ParagraphStyle('hdr',fontName='DV-B',fontSize=11,textColor=WHITE))]],
                colWidths=[TW])
    hdr.setStyle(hdr_ts)
    E += [hdr, sp(6),
          Paragraph('Four frameworks, one event —\nand the main causality axiom becomes a theorem',
                    CS['title']),
          Paragraph('Bridge Document | DA-1 / T-SNAP Update', CS['subtitle']),
          Paragraph('ZP Companion | Version ' + VERSION + ' | April 2026', CS['meta']),
          Paragraph(
              'This companion explains the ideas in plain language with diagrams and real-world '
              'examples. It is not the formal document — every claim here restates a result '
              'already proved in the corresponding technical document. Consult that document for '
              'the authoritative mathematics.', CS['disc'])]

    # What Is ZP-E Doing?
    E.append(Paragraph('What Is ZP-E Doing?', CS['h1']))
    E.append(cbody(
        'ZP-E is the cross-framework synthesis. Written last — after ZP-A through ZP-D are each '
        'internally closed — its job is to show that the four independent frameworks all describe '
        'the same event: the Binary Snap, from four different mathematical vantage points.'))
    E.append(cbody(
        'ZP-E does not re-derive anything. It imports closed results from each sub-document and '
        'shows their consistency. Where a cross-framework connection requires an assumption, '
        'that assumption is named explicitly as a bridge axiom — not hidden inside the argument.'))
    E.append(sp(4))

    # Four Descriptions
    E.append(Paragraph('The Four Descriptions of the Same Event', CS['h1']))
    E.append(cbody(
        'The Binary Snap — the transition from nothing (⊥) to the first state (ε₀) — looks '
        'different depending on which mathematical language you use. ZP-E\'s central result is '
        'that all four descriptions are consistent: one event, four angles.'))
    E.append(cbody(
        'ε₀ is the proof-theoretic ordinal of Peano Arithmetic, the minimum ordinal whose '
        'well-ordering PA cannot prove. Goodstein\'s theorem is the standard witness: every '
        'Goodstein sequence eventually terminates, but PA cannot prove this; the proof requires '
        'transfinite induction up to ε₀. The same object has a second characterization as the '
        'minimum fixed point of the map α ↦ ω^α. The Binary Snap arrives at ε₀ via this '
        'fixed-point route, reaching the same object that the PA strength analysis identifies '
        'from the proof-theoretic side.'))
    E.append(four_framework_diagram())
    E.append(ccaption(
        'The Binary Snap (amber center) described simultaneously in all four frameworks. '
        'Each arrow represents an independent mathematical description of the same event.'))
    E.append(sp(4))
    E.append(example_box('Real-world example — A car crash described by four witnesses', [
        'An engineer (forces), a doctor (injuries), a lawyer (liability), and a physicist '
        '(energy) each describe the same crash completely within their own discipline. '
        'ZP-E shows the four mathematical frameworks are in exactly this relationship to '
        'the Binary Snap.',
    ]))
    E.append(remember_box(
        'Remember: The car crash illustrates what it means to describe one event in multiple '
        'frameworks. The Zero Paradox is not about car crashes — the car crash is an analogy '
        'for the forced first transition from &#8869; to &#949;&#8320; in any join-semilattice.'))
    E.append(sp(6))

    # AX-1 → T-SNAP
    E.append(Paragraph('The Central Advance: AX-1 is Now a Theorem', CS['h1']))
    E.append(cbody(
        'In earlier versions, the Binary Snap causality was listed as AX-1 — an axiom: a '
        'foundational assumption that could not be derived. The claim was: when P₀ is reached, '
        'the Snap happens. Why? Because AX-1 says so.'))
    E.append(cbody(
        'The DA-1 insert changes this. The argument is now complete: reaching P₀ means a '
        'live machine configuration exists (DA-1). Any live configuration passes through c₁ '
        '(definition). c₁ is non-null (L-RUN). No program avoids this (TQ-IH). A non-null '
        'state change from ⊥ is the Binary Snap (ZP-A D2). The Snap is derived — not assumed.'))
    E.append(cbody(
        'DA-1 is now a Derived Proposition rather than a freestanding Design Principle. '
        'Previously DA-1 was an honest but freestanding commitment: "a configuration at P₀ '
        'is necessarily executing." Now it follows from ZP-A CC-2: ⊥ = {⊥}. The bottom element ⊥ '
        'is a Quine atom — a self-containing object with no external position from which it '
        'could be interpreted as a static description. A thing that interprets itself cannot '
        'be waiting for an external interpreter. So ⊥ at P₀ is necessarily executing. '
        'The design commitment has become a derivation.'))
    E.append(cbody(
        '<b>The two-layer structure of DA-1:</b> DA-1 rests on two explicit layers. '
        'The first is the formal conditional: DP-2 (Execution Distinguishability) establishes '
        'that machine states carry execution history independently of output values. From DP-2, '
        'Lean 4 can derive <i>da1_minimal_path</i> — a proof that before and after instantiation '
        'produce the same output value (c₀) while the machine state changes (c₀ → c₁). '
        '`#print axioms` confirms zero axiom dependencies. This is the first Lean formalization '
        'of the core DA-1 claim, not just the surrounding algebra. '
        'The second layer asks: does ⊥ actually satisfy DP-2\'s precondition? '
        'That case rests on three converging arguments.'))
    E.append(cbody(
        '<b>Three paths to the precondition:</b> '
        '(1) CC-2/R3 (ZP-A): ⊥ = {⊥} is a Quine atom — it interprets itself, leaving no '
        'external position from which it could be read as a static description (above). '
        '(2) L-INF (ZP-C): the surprisal of ⊥ diverges to infinity — no finite static '
        'distribution can represent ⊥. '
        '(3) AIT bridge: at the incompressibility threshold P₀, the description of ⊥ '
        'is maximally incompressible — K(c₁|n)/|c₁| = 1. A string that cannot be compressed '
        'beyond itself must be its own execution; a static-description reading is ruled out by '
        'information theory alone. '
        'All three share D7\'s static/executing dichotomy as background and none is circular '
        'with DP-2.'))
    E.append(cbody(
        '<b>Lean 4 formal closure (ZP-K):</b> The three paths are not only conceptually '
        'convincing — two of them are now machine-checked. ZP-K adds a KleeneStructure instance '
        'for MachinePhase: it provides a concrete computational Quine (a code that is its own '
        'program, via Kleene\'s second recursion theorem), and proves that this Quine and the '
        'AFA self-containment argument are the same structural fact in two different languages. '
        'The result is <i>da1_closed_concrete</i>: in Lean 4, '
        'IsQuineAtom(&#8869; : MachinePhase) is a proved theorem. '
        'Path 1 (AFA self-execution) and Path 3 (computational Kleene fixed point) are now '
        'formally IN LEAN SCOPE. Path 2 (informational bridge — unbounded surprisal → necessarily '
        'executing) remains a structural claim outside current Lean formalization. '
        'The formal grounding of DA-1 is therefore: DP-2 plus two Lean-verified structural paths.'))
    E.append(tsnap_chain_diagram())
    E.append(ccaption(
        'The T-SNAP derivation chain: six steps, no axioms beyond AX-B1 and the definition '
        'of a Turing machine. AX-1 (amber) is now a theorem.'))
    E.append(sp(4))
    E.append(example_box('Real-world example — A legal case that becomes undeniable', [
        'A court case starts with an assumption: "the defendant was at the scene." Then '
        'surveillance footage, phone records, and witness testimony all confirm it. The '
        'assumption becomes a proven fact. T-SNAP is the mathematical equivalent: what was '
        'assumed (AX-1) is now proven (T-SNAP) by an independent chain of evidence.',
    ]))
    E.append(sp(8))

    # Remaining Commitments
    E.append(Paragraph('What the Framework Still Assumes', CS['h1']))
    E.append(cbody(
        'After T-SNAP, the framework rests on exactly three commitments — '
        'none of them novel starting assumptions:'))
    E.append(axioms_table())
    E.append(sp(6))
    E.append(cbody(
        'AX-1 is no longer on this list. The framework makes no stronger claim than it has to.'))
    E.append(sp(8))
    E.append(remember_box(
        'Remember: The structural results — monotonicity, clopen separation, '
        'informational singularity, orthogonal shifts — hold in any instantiation of the '
        'framework. The framework makes no claims about which physical theory, if any, '
        'instantiates it.'))

    print(f'Building: {out_path}')
    doc.build(E)
    print(f'Done. File size: {os.path.getsize(out_path) // 1024} KB')

if __name__ == '__main__':
    build()