"""
Build ZP-A: Lattice Algebra (v1.14)
v1.14: CC-2 label updated — "Conditional Claim" → "Forced Metatheoretic Commitment".
Metatheoretic choice of ZF+AFA over Foundation is not free: ruled out by R3 and ZP-C L-INF.
Lean 4 scope note extended — ZPJ_ScaleBridge formally verifies the fixed-point content
(selfMem_eq_singleton_free, z2_selfMem_singleton) in ZFC; set-theoretic interpretation
remains outside Lean scope. Both validation tables updated. No algebraic content changed.
v1.13: OQ-A1b note added distinguishing bounded chains from existence of minimal element
above ⊥. Bounded chains (closed by ZP-E T5 via AX-B1) do not guarantee ε₀ exists as a
minimal non-null element — that is a metric result established by ZP-B, not A1-A4. No
algebraic content changed.
v1.12: OQ-A1b dual-status clarification. The closure note now distinguishes between the
ZP-specific result (bounded by AX-B1 via T5) and the general semilattice case (unbounded
chains are permitted in a bare join-semilattice without AX-B1). Section header updated to
"CLOSED within ZP". No algebraic content changed.
v1.11: ZF+AFA metatheoretic declaration added before Section I; plain English preface added
immediately before CC-1 (§4.2). No mathematical content changed.
v1.10: CC-1 box title updated — "Conditional Claim CC-1" replaced with "CC-1 (Derived/Conditional)"
to avoid reading inconsistency for readers of ZP-A in isolation. The status row inside the box
already accurately states the dual status; the title now reflects it at first glance.
v1.9: CC-1 status updated — now derived as a structural consequence in AFAStructure lattices
via ZP-J T-EXEC (IsQuineAtom(⊥) is unique; S₀ = ⊥ follows structurally). Status line and
validation table updated. Remains a modelling commitment at the ZP-A level without AFAStructure.
v1.8: CC-2 cross-framework note added — Foundation incompatibility with R3 and L-INF noted;
AFA identified as forced rather than chosen. Foundation note in Section V updated accordingly.
Cross-reference to ZP-E Remark R-AFA.
v1.7: R3 dependency note added — the inference "no external interpreter → necessarily executing"
requires D7's exhaustive static/executing dichotomy (ZP-E) as background. R3 supplies the
structural route to eliminating the static-description state; D7 supplies the exhaustiveness.
All three DA-1 paths share D7 as background; independence is among their arguments, not from D7.
"""
import os
from zp_utils import *
VERSION = '1.14'
def build():
out_path = os.path.join(PROJECT_ROOT, 'ZP-A_Lattice_Algebra.pdf')
doc = make_doc(out_path, 'ZP-A: Lattice Algebra', 'ZP-A', 'Version ' + VERSION)
E = []
E += [Paragraph('THE ZERO PARADOX', S['title']),
Paragraph('ZP-A: Lattice Algebra', S['subtitle']),
Paragraph('Version ' + VERSION + ' | May 2026', S['subtitle']),
sp(10),
body('This document is self-contained within abstract algebra. No topology, probability, or Hilbert space is imported. Every claim is provable using only the tools of semilattice theory. Cross-framework connections are deferred to ZP-E.'),
body('Illustrated Companion: A paired ZP-A Illustrated Companion document provides concrete examples and visual intuitions for the results in this document. Examples are kept separate from the formal layers to distinguish illustrative material from proofs. The companion is a reading aid; no proof-critical judgements should be drawn from examples alone.'),
sp()]
E.append(label_box('Metatheoretic Declaration — ZF + AFA', [
'This document is stated over ZF + AFA (Zermelo–Fraenkel set theory with Aczel’s Anti-Foundation Axiom). AFA replaces the classical Axiom of Foundation and permits self-containing sets — in particular, sets satisfying x = {x}.',
'Scope: This declaration affects only CC-2 (Section V), which asserts ⊥ = {⊥}. All algebraic results in Sections I–IV are independent of AFA and hold in standard ZF.',
'Standard concrete models (power sets ordered by inclusion, real intervals ordered by max, etc.) satisfy A1–A4 but do not satisfy ⊥ = {⊥}. This is expected — they are models of the algebraic structure, not instantiations of the ZF + AFA metatheory. The self-containment of ⊥ is a set-theoretic claim about what ⊥ is, not an algebraic one.',
'The Axiom of Choice is not assumed. AFA is forced rather than chosen — see Section V and ZP-E Remark R-AFA for the argument.',
]))
E.append(sp(8))
E.append(Paragraph('I. Primitives and Axioms', S['h1']))
E.append(Paragraph('1.1 Signature', S['h2']))
E.append(body('The algebraic signature of the Zero Paradox state space is a triple: (L, ∨, ⊥)'))
E.append(body('L is a non-empty set (the carrier set of states). ∨ : L × L → L is a binary operation called join. ⊥ ∈ L is a distinguished constant called the bottom element.'))
E.append(sp(4))
E.append(label_box('Axiom Block A — Join-Semilattice with Bottom', [
'A1 — Associativity: (x ∨ y) ∨ z = x ∨ (y ∨ z) for all x, y, z ∈ L',
'A2 — Commutativity: x ∨ y = y ∨ x for all x, y ∈ L',
'A3 — Idempotency: x ∨ x = x for all x ∈ L',
'A4 — Identity (Additive): ⊥ ∨ x = x for all x ∈ L',
]))
E.append(sp(4))
E.append(body('A4 is the load-bearing axiom. It makes ⊥ the additive identity of the algebra: the element that contributes nothing to a join and is therefore present in every state as the neutral constituent.'))
E.append(Paragraph('II. The Induced Partial Order', S['h1']))
E.append(Paragraph('2.1 Definition of ≤', S['h2']))
E.append(label_box('Definition D1 — Lattice Order', [
'For x, y ∈ L, define the relation ≤ by:',
'x ≤ y ⟺ x ∨ y = y',
]))
E.append(sp(4))
E.append(label_box('Proposition T1 — ≤ is a Partial Order', [
'Reflexivity: x ≤ x — by A3, x ∨ x = x. ✓',
'Antisymmetry: if x ≤ y and y ≤ x, then x ∨ y = y and y ∨ x = x. By A2, y = x ∨ y = y ∨ x = x. ✓',
'Transitivity: if x ≤ y and y ≤ z, then x ∨ z = x ∨ (y ∨ z) = (x ∨ y) ∨ z = y ∨ z = z, so x ≤ z. ✓',
]))
E.append(sp(4))
E.append(Paragraph('2.2 ⊥ is the Least Element', S['h2']))
E.append(label_box('Lemma T2 — ⊥ is a Global Minimum under ≤', [
'For all x ∈ L: ⊥ ≤ x',
'Proof: By A4, ⊥ ∨ x = x. By D1, this is the definition of ⊥ ≤ x. ✓',
]))
E.append(sp(4))
E.append(body('T2 is the algebraic statement of the foundational claim: ⊥ is not a void that states depart from — it is the minimum element that every state sits above. Since ⊥ ≤ x for all x, and join accumulates from the bottom, ⊥ is algebraically present in every element of L.'))
E.append(Paragraph('III. The Additive Ontology', S['h1']))
E.append(Paragraph('3.1 No Subtraction Operator', S['h2']))
E.append(label_box('Remark R1 — Join-Semilattice vs. Lattice', [
'A full lattice (L, ∨, ∧, ⊥, ⊤) includes a meet operator ∧ and a top element ⊤. The Zero Paradox restricts to the join-semilattice with bottom. The meet operator is excluded because it would allow state reduction — the removal of informational content from a state. The additive ontology requires that no operation decreases informational content.',
]))
E.append(sp(4))
E.append(Paragraph('3.2 Join is the Only State Transition', S['h2']))
E.append(label_box('Definition D2 — State Transition', [
'A state transition is any function f: L → L such that x ≤ f(x) for all x ∈ L.',
'Equivalently, for each x ∈ L, f(x) = x ∨ α for some α ∈ L.',
'Proof of equivalence:',
'(⇒) If x ≤ f(x), then x ∨ f(x) = f(x) by D1. Take α = f(x): then f(x) = x ∨ α. ✓',
'(⇐) If f(x) = x ∨ α for some α ∈ L, then x ∨ f(x) = x ∨ (x ∨ α) = (x ∨ x) ∨ α = x ∨ α = f(x) by A1, A3. By D1, x ≤ f(x). ✓',
]))
E.append(Paragraph('IV. Monotonicity of State Sequences', S['h1']))
E.append(Paragraph('4.1 State Sequences', S['h2']))
E.append(label_box('Definition D3 — State Sequence', [
'A state sequence is a function S: ℕ → L, written (S0, S1, S2, …), such that:',
'Sn+1 = Sn ∨ αn for some αn ∈ L, for all n ∈ ℕ',
]))
E.append(sp(4))
E.append(label_box('Remark R2 — Terminology: State Sequence and Ascending Chain', [
'In the order-theory literature, a sequence (Sn) satisfying Sn ≤ Sn+1 for all n is called an ascending chain. The term "state sequence" is used here in place of "ascending chain" to align with the state-transition framing of ZP-D and ZP-E, where the same structure is introduced as sequences of system states. The two terms denote the same mathematical object. Readers familiar with order theory should read "state sequence" as "ascending chain". For concrete illustrations, see the ZP-A Illustrated Companion.',
]))
E.append(sp(4))
E.append(label_box('Theorem T3 — State Sequences are Monotone', [
'For any state sequence (Sn) satisfying D3: Sn ≤ Sn+1 for all n ∈ ℕ',
'Proof: By D3, Sn+1 = Sn ∨ αn. By D1, Sn ≤ Sn ∨ αn ⟺ Sn ∨ (Sn ∨ αn) = Sn ∨ αn. By A1, (Sn ∨ Sn) ∨ αn = Sn ∨ αn. By A3, Sn ∨ Sn = Sn. Therefore Sn ∨ αn = Sn+1. ✓',
'Monotonicity is a theorem, not a postulate. It is derived from A1–A3 via D3.',
]))
E.append(sp(4))
E.append(Paragraph('4.2 The Initial State', S['h2']))
E.append(body('Every state sequence begins somewhere. T2 establishes ⊥ ≤ S₀ for any initialisation — the bottom element is always below the starting point, whatever that starting point is. But T2 does not fix where S₀ sits; a sequence could legitimately begin above ⊥. CC-1 closes this gap: we commit to initialising at the minimum. This is a modelling choice at ZP-A scope. In the AFAStructure lattices of ZP-J, T-EXEC derives it as a structural consequence rather than an assumption.'))
E.append(label_box('CC-1 — S₀ = ⊥ | Derived in AFAStructure lattices (ZP-J T-EXEC); conditional at ZP-A scope', [
'We commit to initialising every state sequence at the minimum of L: S0 = ⊥. This is not derived from A1–A4 — it is a modelling choice.',
'Under CC-1 and T3: S0 = ⊥ ≤ S1 ≤ S2 ≤ …',
'Note: By T2, ⊥ ≤ S0 for any initialisation — this holds unconditionally from A4. CC-1 strengthens this to equality: S0 = ⊥. The commitment is not needed to establish ⊥ ≤ S0; it is needed to fix the starting point precisely.',
'Status: DERIVED (given AFAStructure grounding) — ZP-J T-EXEC establishes IsQuineAtom(⊥) as the unique structural identity; S0 = ⊥ follows as a structural consequence in any AFAStructure lattice. Modelling commitment at the ZP-A level (no AFAStructure assumption is made within this document).',
]))
E.append(sp(4))
E.append(Paragraph('V. The Self-Containment of ⊥', S['h1']))
E.append(Paragraph('5.1 Foundational Characterisation', S['h2']))
E.append(body('The axioms A1–A4 establish ⊥ as the additive identity and algebraic minimum of L. The following forced metatheoretic commitment characterises its set-theoretic nature. R3 provides a structural route to DA-1 in ZP-E: CC-2 establishes that ⊥ has no external interpreter position, which — conditional on D7’s exhaustive static/executing dichotomy (ZP-E) as background — eliminates the static-description state for ⊥. See R3 for the full dependency note.'))
E.append(body('Foundation note: The framework is stated over ZF + AFA (Zermelo–Fraenkel set theory with Aczel’s Anti-Foundation Axiom). The classical Axiom of Foundation is replaced by AFA, which permits self-containing sets. This replacement is not an arbitrary modelling choice: ZF + Foundation is incompatible with CC-2 (a well-founded ⊥ would admit an external interpreter, contradicting R3) and with ZP-C L-INF (bounded ∈-rank contradicts unbounded surprisal of ⊥). See ZP-E Remark R-AFA for the full cross-framework argument. The Axiom of Choice is not assumed.'))
E.append(sp(4))
E.append(label_box('Forced Metatheoretic Commitment CC-2 — Self-Containment of ⊥', [
'The null state ⊥ is its own extension: the collection of all objects bearing the structural property of ⊥ is ⊥ itself.',
'Formally: ⊥ = {⊥}',
'Under ZF + AFA, ⊥ is a Quine atom — a set satisfying x = {x}. By set extensionality, any infinite collection of objects all indistinguishable under the structural property of ⊥ collapses to ⊥ itself. There is no multiplicity, only ⊥.',
'This is a forced metatheoretic commitment, not a freely chosen modeling decision. The replacement of Foundation by AFA is structurally required — Foundation is ruled out by R3 and ZP-C L-INF. It is not derived from A1–A4 at the algebraic level; the metatheoretic choice is forced at the framework level.',
'Status: FORCED METATHEORETIC COMMITMENT — AFA over Foundation is structurally required, not freely chosen. Algebraic fixed-point content formally verified in ZFC by ZP-J (ZPJ_ScaleBridge); set-theoretic interpretation outside Lean scope.',
'Cross-framework note: The replacement of Foundation by AFA is not an arbitrary choice — ZF + Foundation is ruled out by R3 (a well-founded ⊥ would admit an external interpreter, contradicting CC-2) and by ZP-C L-INF (bounded ∈-rank contradicts unbounded surprisal of ⊥). Foundation and AFA are dual framings of the same object: Foundation excludes the Quine atom; AFA uniquely permits it. Both axioms converge on the identical object with zero gap between them. AFA is the forced metatheoretic replacement; the specific form ⊥ = {⊥} is the minimal Quine atom consistent with A4. See ZP-E Remark R-AFA for the full cross-framework argument.',
'Lean 4 scope — three distinct layers. (1) Set-theoretic: the claim ⊥ = {⊥} as a set cannot be realized in Lean’s type theory (CIC is well-founded by construction). This remains a prose-level commitment in ZF + AFA. (2) AFAStructure context (conditional on AFA as ambient): ZP-J defines IsQuineAtom as the lattice-theoretic analog — IsQuineAtom q := selfMem q ∧ ∀ x, selfMem x → x = q. Within an AFAStructure instance, t_exec_iff proves IsQuineAtom q ↔ q = ⊥ (ZPJ.lean); ZP-K’s da1_closed_concrete closes this concretely on MachinePhase. These results assume AFAStructure as ambient context — they are conditional on AFA structure, not derived independently of it. (3) ZFC-clean (no AFA import): ZPJ_ScaleBridge.lean proves the fixed-point content in standard ZFC — selfMem_eq_singleton_free and z2_selfMem_singleton establish {x : ℤ₂ | 2x = x} = {0}. This result is loop-free from AFA. The set-theoretic interpretation connecting layer 3 to layer 1 remains outside Lean scope.',
]))
E.append(sp(4))
E.append(label_box('Remark R3 — CC-2 Eliminates the Static-Description State for ⊥', [
'A self-containing object has no external interpreter by structure: ⊥ = {⊥} is its own interpretation. A description requires a describer distinct from the thing described; CC-2 admits no such distinction for ⊥. Under the Turing model framework (D7, ZP-E), which partitions machine configurations into static-description states and executing states, the absence of any external interpreter position means ⊥ cannot occupy D7’s static-description category.',
'Dependency note: The inference from "no external interpreter" to "necessarily executing" uses D7’s exhaustiveness in the final step — that static-description and executing are the only two categories. D7 (ZP-E) supplies this exhaustiveness as the shared background framework. R3 provides the structural argument for why ⊥ engages D7’s transition; it does not independently derive DA-1 without D7. All three DA-1 paths in ZP-E share D7 as background. Their independence is among their arguments — CC-2/R3 (structural), L-INF (informational), K-incompressibility (AIT) — not from D7 itself.',
]))
E.append(sp())
E.append(Paragraph('VI. OQ-A1 — Sufficiency of Monotonicity', S['h1']))
E.append(label_box('OQ-A1 — Sufficiency of Monotonicity [CLOSED within ZP — ZP-E T5]', [
'Is the monotonicity constraint (T3) sufficient to characterise all valid state sequences, or are additional axioms required?',
'OQ-A1a: Is there algebraic reason to restrict αn to join-irreducible elements (not expressible as joins of strictly smaller elements)?',
'OQ-A1b: Does the open-ended semilattice (without top element ⊤) permit unbounded ascending chains?',
'Status: CLOSED within ZP — Both sub-questions resolved by ZP-E Theorem T5 (Iterative Forcing Theorem) via AX-B1 from ZP-B. OQ-A1a: αn = ε(Sn), the minimum viable deviation (ZP-specific). OQ-A1b: Within ZP, AX-B1\'s binary constraint bounds ascending chains via T5. Note: in general semilattice theory without AX-B1, unbounded ascending chains are permitted — a bare join-semilattice imposes no bound. The closure here is a consequence of ZP\'s binary existence commitment, not of A1–A4 alone.',
'Note on minimal element above ⊥: Bounded chains do not in themselves guarantee a minimal element above ⊥. In a dense structure, for any ε > 0, ε/2 also exists — chains may be bounded yet have no first step. The closure of OQ-A1b establishes that ascending chains are bounded within ZP; it does not establish that ε₀ exists as a specific minimal non-null element. That existence is a metric result, established by ZP-B’s 2-adic structure, which places 0 at infinite valuation and every non-zero element at finite valuation. The gap between them is not bridgeable by halving. This is outside the scope of A1–A4.',
]))
E.append(Paragraph('VII. Boundary Conditions', S['h1']))
E.append(data_table(
['Export', 'Status / Receiving Document'],
[['(L, ∨, ⊥) as join-semilattice', 'Derived (A1–A4) — ZP-D: algebraic structure of state space'],
['≤ partial order (D1, T1)', 'Derived — ZP-D: ordering on states'],
['Monotonicity of state sequences (T3)', 'Derived from A1–A3 — ZP-D: state layer ordering'],
['⊥ as global minimum (T2, CC-1)', 'Derived / Conditional — ZP-E: ontological grounding claim. CC-1 now derived in AFAStructure lattices via ZP-J T-EXEC.'],
['⊥ = {⊥} self-containment (CC-2, R3)', 'Forced Metatheoretic / Remark — ZP-E: structural route to eliminating static-description state for ⊥, given D7 exhaustiveness as background. Fixed-point content verified in ZFC by ZP-J.'],
['No subtraction / additive ontology (R1)', 'Structural — ZP-C: no operation may reduce informational content'],
['OQ-A1 — increment selection', 'Open within ZP-A; closed by ZP-E T5']],
[2.5*inch, 4.0*inch]
))
E.append(Paragraph('VIII. Validation Status', S['h1']))
E.append(data_table(
['Component', 'Status / Notes'],
[['A1–A4 join-semilattice axioms', 'Valid — Axioms; self-contained'],
['≤ partial order (D1, T1)', 'Valid — Derived from A1–A3'],
['⊥ as least element (T2)', 'Valid — Derived from A4 and D1'],
['Additive ontology / no subtraction (R1)', 'Valid — Structural; signature restriction'],
['State transition as join (D2)', 'Valid — Defined; consistent with signature'],
['Monotonicity of state sequences (T3)', 'Valid — Derived from A1–A3 and D3'],
['CC-1: S0 = ⊥', 'DERIVED (given AFAStructure grounding, ZP-J T-EXEC) — structural consequence in any AFAStructure lattice. Modelling commitment at ZP-A level without AFAStructure assumption.'],
['CC-2: ⊥ = {⊥}', 'Forced Metatheoretic Commitment — AFA over Foundation structurally required; fixed-point content verified in ZFC by ZPJ_ScaleBridge'],
['ZF + AFA foundation (no AC)', 'Meta-theoretic — framework-wide; required for CC-2'],
['OQ-A1: Sufficiency of monotonicity', 'Open within ZP-A; closed by ZP-E T5']],
[2.5*inch, 4.0*inch]
))
doc.build(E)
print(f'Built: {out_path} ({os.path.getsize(out_path) // 1024} KB)')
if __name__ == '__main__':
build()