"""
Zero Paradox — ZP-J: Executability of Self-Reference PDF Builder
Version 2.1 | May 2026
v2.1: Version changelog removed from preamble; version stripped from section headers and endnote.
v2.0: Four new sections added — Section VII (Aczel DC-free connection),
Section VIII (abstraction chain: ValuationStructure → AbstractSelfApp →
AFAStructure), Section IX (concrete instances: ℕ∞ and OntologicalStates),
Section X (APG decoration uniqueness). All new content proved sorry-free in
Lean 4 across ZPJ_AczelConn.lean, ZPJ_SelfApp.lean, ZPJ_Scale.lean,
ZPJ_Model.lean, ZPJ_OntBridge.lean, ZPJ_APG.lean.
v1.2: Minor wording fix — "not an asserted coincidence" removed from preamble.
v1.1: Remark R-J.0 added — CIC encoding scope. AFAStructure concrete instances
item CLOSED — ZP-K provides machinePhaseAFA.
v1.0: Initial release — Theorem T-EXEC; all ZPJ.lean theorems axiom-free.
"""
import os
from zp_utils import *
VERSION = '2.1'
def build():
out_path = os.path.join(PROJECT_ROOT, 'ZP-J_Self_Reference.pdf')
doc = make_doc(out_path,
'ZP-J: Executability of Self-Reference',
'ZP-J: Executability of Self-Reference',
'Version ' + VERSION)
E = []
print('[build_zpj] Building title block...')
E += [
sp(12),
Paragraph('THE ZERO PARADOX', S['title']),
Paragraph('ZP-J: Executability of Self-Reference', S['title']),
Paragraph('Version ' + VERSION + ' | May 2026', S['subtitle']),
sp(10),
hr(),
sp(4),
]
E.append(body(
'This document establishes Theorem T-EXEC (Executability of Self-Reference): in any '
'ZP-A join-semilattice with AFA (Anti-Foundation Axiom) grounding, the unique Quine atom '
'Q — the element satisfying Q = {Q} — is provably the bottom element ⊥. '
'This closes the bridge between the set-theoretic and order-theoretic layers of the '
'framework. CC-1 from ZP-A, which stated "S₀ = ⊥" as a modelling commitment, '
'becomes a derived theorem.'))
E.append(body(
'Version 2.0 extends the core T-EXEC result in four directions: it establishes that '
'Aczel\'s use of Dependent Choice is unnecessary for the self-membership case (Section VII); '
'it generalises the AFAStructure typeclass into an abstraction chain reaching down to '
'a pure valuation structure (Section VIII); it instantiates that chain on two concrete '
'types (Section IX); and it proves global decoration uniqueness for finite accessible '
'pointed graphs (Section X). All results are sorry-free in Lean 4.',
style='bodyI'))
E.append(hr())
print('[build_zpj] Building Section I...')
E += [
Paragraph('Section I: The Open Question — CC-1 as a Modelling Commitment', S['h1']),
hr(),
]
E.append(Paragraph('I. CC-1 in ZP-A', S['h2']))
E.append(body(
'ZP-A Conditional Claim CC-1 states: if the state sequence is initialised at ⊥, '
'then ⊥ ≤ S(n) for all n. This follows trivially from T2 (⊥ is the '
'global minimum), so its formal content is essentially: we are choosing ⊥ as the '
'initial state S₀.'))
E.append(body(
'The label "Conditional Claim" (CC) marks this as a modelling commitment — an '
'explicit choice not derivable from the axioms A1–A4 alone. ZP-A\'s axioms give us '
'a semilattice with a bottom element. They do not say which instantiation of the '
'semilattice should start at that bottom. CC-1 asserts: ours does. This is '
'well-motivated, but it is a choice.'))
E.append(body(
'The question ZP-J investigates: is this choice forced? Is there a structural reason — '
'derivable from the framework\'s foundational commitments — that any well-grounded '
'instantiation of ZP-A must begin at ⊥? The answer is yes, provided the lattice '
'has AFA grounding.'))
E.append(Paragraph('II. The Implicit Identification', S['h2']))
E.append(body(
'ZP-E\'s DA-1 Path 1 already states: ⊥ = {⊥} (Quine atom, ZF+AFA). This '
'identification — the bottom element is the unique self-containing set under AFA — '
'was present informally but never formally bridged to CC-1. It appeared as motivation for '
'why ⊥ is the right starting point, not as a derivation of it.'))
E.append(body(
'The gap: ZP-A\'s lattice order is abstract (defined by axioms A1–A4). AFA is a '
'set-theoretic axiom. There is no automatic connection between "x is self-containing" '
'and "x is the lattice bottom." Connecting them requires a bridge — and that bridge '
'was the missing piece. ZP-J provides it.'))
E.append(callout(
'Open question entering ZP-J: Is CC-1 (S₀ = ⊥) forced by the framework\'s '
'foundational structure, or is it an independent modelling choice? '
'If forced, what is the structural reason? '
'Answer (ZP-J T-EXEC): it is forced — by the AFA identification ⊥ = {⊥}, '
'encoded structurally in the AFAStructure typeclass.',
bg=AMBER_LITE, border=AMBER
))
E.append(sp(6))
print('[build_zpj] Building Section II...')
E += [
hr(),
Paragraph('Section II: AFA Machinery — Self-Membership and the Quine Atom', S['h1']),
hr(),
]
E.append(Paragraph('I. The Anti-Foundation Axiom', S['h2']))
E.append(body(
'Standard set theory (ZF) includes the Foundation Axiom: every non-empty set S contains '
'an element disjoint from S. A consequence is that no set can contain itself: x ∈ x '
'is impossible in ZF. This rules out self-referential sets by fiat.'))
E.append(body(
'The Anti-Foundation Axiom (AFA, Aczel 1988) replaces Foundation with a universal '
'existence and uniqueness result: every accessible pointed graph (APG) has a unique '
'set-theoretic decoration. Under AFA, self-containing sets are not only possible but '
'uniquely characterised. The resulting theory ZF+AFA is consistent and expressive — '
'it is the natural set-theoretic home for fixed-point and self-referential structures.'))
E.append(Paragraph('II. The Quine Atom', S['h2']))
E.append(body(
'Under AFA, the equation x = {x} has a unique solution. This solution is called the '
'Quine atom, denoted Q. Q is the unique set that contains itself as its sole member: '
'Q = {Q}. It is not the empty set (∅ = {} contains nothing); it is not any '
'well-founded set (those cannot contain themselves). Q is the minimal non-trivial AFA '
'set — it contains exactly one thing, and that thing is itself.'))
E.append(body(
'The AFA uniqueness guarantee is the key property: there is at most one Quine atom. '
'Any two self-containing elements are equal. This means the self-membership property '
'uniquely identifies an element — a fingerprint that belongs to exactly one object '
'in the universe.'))
E.append(axiom_box(
'AFA Uniqueness (AFAStructure.quine_unique)',
[
'For any type L with AFA structure: if x, y ∈ L both satisfy selfMem(x) and '
'selfMem(y), then x = y.',
'Informally: the Quine atom is unique. Self-containment is a property held by at '
'most one element of any AFA-structured type.',
'Lean: AFAStructure.quine_unique — encoded as a typeclass field, not a theorem, '
'because AFA is a foundational axiom and cannot be derived from type-theoretic '
'principles alone. It is a structural prerequisite for any AFA-grounded lattice.',
]
))
E.append(sp(6))
E.append(Paragraph('III. Self-Membership as a Lattice Predicate', S['h2']))
E.append(body(
'In ZP-J, the AFA machinery is abstracted minimally. We do not need the full apparatus '
'of accessible pointed graphs, bisimulation, or set decoration. We need only two things: '
'a predicate selfMem on the lattice elements, and the guarantee that it is held '
'by at most one element (quine_unique). The third structural field — bot_self_mem — '
'is where the bridge is built.'))
E.append(body(
'The AFAStructure typeclass in ZPJ.lean captures exactly this. Its three fields are '
'sufficient to derive T-EXEC with no additional axioms. The full AFA machinery '
'(APGs, bisimulation, decoration) provides the informal justification for why any '
'concrete lattice grounded in ZF+AFA satisfies these three fields — but the formal '
'derivation requires only the fields themselves.'))
print('[build_zpj] Building Section III...')
E += [
hr(),
Paragraph('Section III: AFAStructure — The Structural Bridge', S['h1']),
hr(),
]
E.append(Paragraph('I. The Three Fields', S['h2']))
E.append(body(
'The AFAStructure typeclass for a ZP-A semilattice L has three fields. The first two '
'encode standard AFA properties. The third is the bridge.'))
E.append(def_box(
'AFAStructure Typeclass (ZPJ.lean § I)',
[
'class AFAStructure (L : Type*) [ZPSemilattice L] with:',
'(1) selfMem : L → Prop '
'— the self-membership predicate. selfMem(x) means x contains itself as a member '
'in the AFA sense.',
'(2) quine_unique : ∀ x y : L, selfMem(x) → selfMem(y) → x = y '
'— AFA uniqueness. At most one element of L is self-containing.',
'(3) bot_self_mem : selfMem(⊥) '
'— the bridge field. The bottom element of the lattice is self-containing. '
'This is the formal encoding of ⊥ = {⊥}.',
]
))
E.append(sp(6))
E.append(Paragraph('II. What bot_self_mem Says', S['h2']))
E.append(body(
'bot_self_mem is the single structural claim that connects the order-theoretic world '
'(ZP-A\'s lattice) to the set-theoretic world (AFA). It says: the bottom element ⊥ '
'of the lattice is self-containing — it satisfies selfMem(⊥).'))
E.append(body(
'In set-theoretic terms: ⊥ ∈ ⊥, i.e. ⊥ = {⊥}. '
'In the framework: ⊥ contains itself as its sole content. '
'This is not a new claim — it is the identification that ZP-E\'s DA-1 Path 1 already '
'invokes informally. ZP-J encodes it as a typeclass field, making it a verifiable '
'structural prerequisite rather than a narrative motivation.'))
E.append(body(
'Any concrete lattice L that claims to be AFA-grounded must prove bot_self_mem as '
'part of its AFAStructure instance. If it cannot, it is not genuinely AFA-grounded — '
'the identification ⊥ = {⊥} is part of what "AFA-grounded" means.'))
E.append(remark_box(
'Remark R-J.0 — CIC Encoding and the AFA Distinction',
[
'In the MachinePhase concrete instance (ZP-K), selfMem is defined as '
'selfMem x := x = ⊥. With this definition, bot_self_mem is proved by rfl: '
'⊥ = ⊥ holds by reflexivity.',
'This is the CIC-compatible encoding of AFA self-containment. In Lean 4 (based on '
'the Calculus of Inductive Constructions), the set-theoretic statement ⊥ ∈ ⊥ '
'— meaning ⊥ literally contains itself as a member under ZF+AFA — is not '
'directly formalizable. CIC lacks the membership relation ∈ of set theory. The '
'encoding selfMem x := x = ⊥ captures the structural role: "self-containing" '
'means "equals the bottom element." The Lean proof compiles by rfl because '
'self-containing is defined as equality with ⊥.',
'This is a structural analogy, not a set-theoretic derivation from ZF+AFA. The '
'full set-theoretic content of AFA — that ⊥ literally contains itself as a '
'member of the AFA universe — is not present in the Lean proof. What the typeclass '
'encodes is the structural consequence: there is a unique element playing the Quine '
'role, and ⊥ is that element.',
]
))
E.append(sp(6))
E.append(Paragraph('III. Why a Typeclass Field Rather than a Freestanding Axiom', S['h2']))
E.append(body(
'In the stub version of ZPJ.lean, the bridge was a freestanding axiom: '
'ax_j1_quine_join_identity. It stated directly that the Quine atom satisfies the '
'join-identity. This compiled, but the purity check showed T-EXEC depending on '
'ax_j1_quine_join_identity — a named axiom floating outside any typeclass.'))
E.append(body(
'Encoding the commitment as a typeclass field is philosophically and formally cleaner. '
'A freestanding axiom is a global assertion that the proof checker accepts without '
'verification. A typeclass field is a requirement: any instance of AFAStructure must '
'supply a proof of bot_self_mem. The commitment is not asserted once and forgotten — '
'it is checked at every instantiation. Concrete lattices must earn their AFA status.'))
E.append(callout(
'The distinction: a freestanding axiom says "trust me, this is true." '
'A typeclass field says "prove it for your specific lattice, or it does not compile." '
'ZP-J uses the second. The philosophical commitment (⊥ = {⊥}) '
'becomes a proof obligation at every concrete instantiation.',
bg=SLATE_LITE, border=SLATE
))
E.append(sp(6))
print('[build_zpj] Building Section IV...')
E += [
hr(),
Paragraph('Section IV: Theorem T-EXEC — The Quine Atom is Bottom', S['h1']),
hr(),
]
E.append(result_box(
'Theorem T-EXEC — Executability of Self-Reference',
[
'Statement: Let L be a ZP-A semilattice with AFAStructure. '
'If q : L is a Quine atom (selfMem(q) and q is unique among self-containing '
'elements), then q = ⊥.',
'Lean: ZeroParadox.ZPJ.t_exec — proved in ZPJ.lean. '
'Purity: does not depend on any axioms. ✓',
]
))
E.append(sp(8))
E.append(Paragraph('I. The Proof', S['h2']))
E.append(body(
'The proof of T-EXEC is immediate from the typeclass fields. It has three steps:'))
E += [
li('hq.2 states: every self-containing element of L equals q. '
'(This is the uniqueness half of IsQuineAtom q.)'),
li('AFAStructure.bot_self_mem states: ⊥ is self-containing. '
'(This is the bridge field — ⊥ = {⊥} encoded structurally.)'),
li('Applying hq.2 to ⊥ using bot_self_mem gives: ⊥ = q. '
'By symmetry: q = ⊥. QED.'),
sp(4),
]
E.append(body(
'The entire proof is one line in Lean 4: '
'(hq.2 bot AFAStructure.bot_self_mem).symm. '
'No appeal to the join operation. No bridge axiom. No DA-2. '
'Just AFA uniqueness applied at ⊥.'))
E.append(remark_box(
'Remark R-J.1',
[
'The proof does not use da2_bottom_characterization (from ZP-E). '
'That result — "(∀ x, join S x = x) ↔ S = ⊥" — is used in '
'the derived theorem J1 (Section V), but T-EXEC itself is purely order-theoretic: '
'it uses only quine_unique and bot_self_mem.',
]
))
E.append(sp(6))
E.append(Paragraph('II. IsQuineAtom bot', S['h2']))
E.append(body(
'A corollary of T-EXEC is that ⊥ itself is a Quine atom. This is the converse '
'direction: not only does the Quine atom equal ⊥ (T-EXEC), but ⊥ equals '
'the Quine atom (bot_is_quine_atom).'))
E.append(result_box(
'Proposition — bot_is_quine_atom',
[
'In any AFAStructure lattice L: IsQuineAtom(⊥).',
'Proof: ⊥ is self-containing by bot_self_mem. Any other self-containing '
'x satisfies x = ⊥ by quine_unique(x, ⊥, selfMem(x), bot_self_mem).',
'Lean: ZeroParadox.ZPJ.bot_is_quine_atom — does not depend on any axioms. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('III. The Full Biconditional', S['h2']))
E.append(body(
'Combining T-EXEC and bot_is_quine_atom yields the full biconditional: '
'IsQuineAtom(q) ↔ q = ⊥. Being the Quine atom and being the bottom element '
'are the same property, stated in set-theoretic and order-theoretic language respectively.'))
E.append(result_box(
'Theorem t_exec_iff — Full Equivalence',
[
'For any q : L in an AFAStructure lattice:',
'IsQuineAtom(q) ↔ q = ⊥ ↔ ∀ x : L, join q x = x.',
'The three conditions are mutually equivalent: Quine atom (set-theoretic), '
'bottom element (order-theoretic), and join-identity element (algebraic). '
'They are three formulations of one structural role.',
'Lean: ZeroParadox.ZPJ.t_exec_iff — does not depend on any axioms. ✓',
]
))
E.append(sp(6))
print('[build_zpj] Building Section V...')
E += [
hr(),
Paragraph('Section V: Derived Results — J1 and CC-1 as Theorems', S['h1']),
hr(),
]
E.append(Paragraph('I. J1 — QuineJoinIdentity (Derived)', S['h2']))
E.append(body(
'In the initial stub of ZPJ.lean, the claim "the Quine atom satisfies the join-identity" '
'was stated as a freestanding axiom (ax_j1_quine_join_identity). ZP-J replaces it with '
'a theorem.'))
E.append(result_box(
'Theorem J1 — QuineJoinIdentity (formerly Axiom AX-J1)',
[
'In any AFAStructure lattice L, if q is the Quine atom, then ∀ x : L, join q x = x.',
'Proof: q = ⊥ by T-EXEC. Then join q x = join ⊥ x = x by A4 (bot_join, ZP-A). ✓',
'Status: DERIVED THEOREM. Was axiom ax_j1_quine_join_identity in the stub — '
'now proved from T-EXEC + ZP-A A4. No freestanding axiom remains.',
'Lean: ZeroParadox.ZPJ.j1_quine_join_identity — does not depend on any axioms. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('II. CC-1 Derived', S['h2']))
E.append(body(
'ZP-A CC-1 is now a theorem. If the initial state S₀ of a state sequence is the '
'Quine atom Q, then S₀ = ⊥ — a consequence of T-EXEC, not a modelling '
'choice.'))
E.append(result_box(
'Theorem CC-1 (Derived) — cc1_derived',
[
'Let L be an AFAStructure lattice. Let S : ℕ → L be a state sequence '
'(ZP-A D3) and Q : L a Quine atom. If S(0) = Q, then S(0) = ⊥.',
'Proof: S(0) = Q (hypothesis). Q = ⊥ by T-EXEC. Therefore S(0) = ⊥.',
'The modelling commitment "we choose ⊥ as the initial state" is replaced by '
'"the Quine atom IS ⊥, structurally." Starting at Q and starting at ⊥ '
'are not two choices — they are the same state, identified by structure.',
'Lean: ZeroParadox.ZPJ.cc1_derived — does not depend on any axioms. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('III. Uniqueness of the Bottom Role', S['h2']))
E.append(body(
'A further consequence is algebraic uniqueness: in any ZP-A semilattice (without even '
'requiring AFA structure), at most one element can satisfy the join-identity. '
'This is a clean corollary of da2_bottom_characterization (ZP-E).'))
E.append(result_box(
'Theorem — bot_unique',
[
'For any ZP-A semilattice L (no AFA required): if x, y : L both satisfy '
'∀ z, join x z = z and ∀ z, join y z = z, then x = y.',
'Proof: da2_bottom_characterization gives x = ⊥ and y = ⊥. Therefore x = y.',
'Lean: ZeroParadox.ZPJ.bot_unique — does not depend on any axioms. ✓',
]
))
E.append(sp(6))
print('[build_zpj] Building Section VI...')
E += [
hr(),
Paragraph('Section VI: Implications — What Was the Commitment?', S['h1']),
hr(),
]
E.append(Paragraph('I. The Remaining Foundation', S['h2']))
E.append(body(
'T-EXEC and its corollaries carry zero freestanding axioms in the Lean 4 purity check. '
'The entire derivation traces to the fields of two typeclasses: ZPSemilattice (from ZP-A) '
'and AFAStructure (new in ZP-J). No standalone axiom statement appears anywhere in the '
'ZPJ.lean proof obligations.'))
E.append(body(
'The foundational commitments are the typeclass fields themselves. In ZPSemilattice: '
'A1–A4 (the semilattice axioms). In AFAStructure: selfMem (a predicate), '
'quine_unique (AFA uniqueness), and bot_self_mem (the bridge). These are the structural '
'prerequisites for any lattice that claims ZP-A + AFA grounding. They are not axioms '
'floating in the ambient theory — they are proof obligations that any concrete '
'instance must discharge.'))
E.append(Paragraph('II. Where the Philosophy Lives Now', S['h2']))
E.append(body(
'The philosophical content of ⊥ = {⊥} has not disappeared. It has moved. '
'Previously it lived in a narrative comment in ZP-A (CC-1\'s informal motivation) and '
'in ZP-E\'s DA-1 Path 1 (one of three informal arguments for instantiation as execution). '
'Now it lives in the definition of AFAStructure itself — specifically in bot_self_mem.'))
E.append(body(
'This is the correct location for a foundational claim. It is not hidden in a proof; '
'it is stated in the typeclass definition where any reader can see it. Any lattice that '
'wants to use ZP-J\'s results must provide a proof that its bottom element is '
'self-containing. If it cannot, it is simply not an AFA-grounded lattice in the '
'sense required by this framework.'))
E.append(Paragraph('III. The Formal Chain', S['h2']))
E.append(body(
'The derivation chain entering ZP-J had one remaining gap: CC-1 was a committed '
'starting point, not a derived one. Sections I–VI close that gap. '
'Sections VII–X extend the chain further: they reduce the axiom load of '
'AFAStructure, provide concrete models, and prove the full AFA decoration uniqueness '
'theorem for finite graphs. Every node is either a proved theorem or a typeclass field:'))
E += [
li('ZP-A axioms A1–A4: semilattice structure (ZPSemilattice fields).'),
li('ZP-B: 2-adic topology and irreversibility (proved from Mathlib).'),
li('ZP-C: information theory, L-INF, L-RUN (proved axiom-free or from Mathlib).'),
li('ZP-D: state layer, orthogonality (proved from ZP-A and ZP-B).'),
li('ZP-E: T-SNAP, DA-1, DA-2 (T-SNAP and DA-2 proved axiom-free; DA-1 Path 3 outside Lean scope).'),
li('ZP-J: AFAStructure fields (selfMem, quine_unique, bot_self_mem). '
'T-EXEC, J1, CC-1: proved axiom-free. '
'v2.0: Sections VII–X (Aczel connection, abstraction chain, concrete instances, '
'decoration uniqueness): all sorry-free. ✓'),
sp(4),
]
E.append(body(
'DA-1 Path 3 (the AIT/Kolmogorov complexity argument in ZP-E) remains outside Lean '
'scope for the same reason it always has: Kolmogorov complexity is uncomputable and '
'absent from Mathlib. ZP-J does not affect DA-1\'s status.'))
E.append(sp(6))
print('[build_zpj] Building Section VII...')
E += [
hr(),
Paragraph('Section VII: The Aczel Connection — DC-Free Results', S['h1']),
hr(),
]
E.append(body(
'Formalised in ZPJ_AczelConn.lean as an immediate extension of the T-EXEC typeclass '
'encoding; the DC-free observation follows directly from quine_unique.',
style='bodyI'))
E.append(sp(4))
E.append(Paragraph('I. Aczel\'s Use of Dependent Choice', S['h2']))
E.append(body(
'Aczel (Non-Well-Founded Sets, 1988, ch. 6) proves that JΦ = ⋃{x | x ⊆ '
'Φx} is the largest pre-fixed-point of a set-continuous operator Φ. The proof uses '
'the axiom of Dependent Choice (DC) to construct an ω-chain, and Aczel explicitly '
'notes: "I do not know if this use of the axiom of dependent choices was essential."'))
E.append(body(
'DC is used when you must build a witness step by step because the fixed point '
'cannot be identified structurally. In ZF+AFA, the Quine atom is unique by the axiom '
'itself. Once uniqueness is available, construction is unnecessary — identification '
'suffices.'))
E.append(Paragraph('II. The J_self Set and Its Structure', S['h2']))
E.append(body(
'In ZP\'s encoding, the analogue of Aczel\'s J∑ for the self-membership operator '
'is J_self = {x : L | selfMem(x)} — the set of self-containing elements. '
'The key results about J_self follow immediately from AFAStructure '
'(Lean: ZPJ_AczelConn.lean § I):'))
E.append(result_box(
'J_self Theorems (ZPJ_AczelConn.lean § I)',
[
'bot ∈ J_self: the bottom element is self-containing. (AFAStructure.bot_self_mem.)',
'J_self_eq_bot: every x ∈ J_self satisfies x = ⊥. '
'(One step: quine_unique x ⊥ hx bot_self_mem.)',
'J_self_eq_singleton_bot: J_self = {⊥}. Proved without DC. ✓',
'J_self_is_largest: for any set S of self-containing elements, S ⊆ J_self. '
'(Aczel 6.5 part (2), self-membership case — without DC.) ✓',
]
))
E.append(sp(6))
E.append(body(
'Where Aczel\'s proof requires an ω-chain to arrive at J∑, the ZP proof is '
'one line: quine_unique applied once identifies the unique self-containing element as '
'⊥. The chain is redundant because the fixed point is forced, not constructed.'))
E.append(Paragraph('III. The Abstract Principle: Uniqueness Eliminates DC', S['h2']))
E.append(body(
'The argument is not specific to self-membership. It holds for any predicate with a '
'unique witness. ZPJ_AczelConn.lean makes this explicit:'))
E.append(result_box(
'Theorem singleton_from_unique_witness (ZPJ_AczelConn.lean § II)',
[
'For any type α and predicate P : α → Prop: '
'if w satisfies P(w) and ∀ x, P(x) → x = w, '
'then {x | P(x)} = {w}.',
'Proof: pure set extensionality. No DC, no Classical.choice. ✓',
'Application: selfMem_determines_singleton — {x : L | selfMem(x)} = {⊥} '
'for any AFAStructure lattice L.',
]
))
E.append(sp(6))
E.append(callout(
'Scope note: the DC-free result applies to the self-membership operator because '
'AFA provides uniqueness (quine_unique) directly. Whether DC can be eliminated for '
'general set-continuous operators Φ depends on whether uniqueness holds for each '
'Φ-fixed-point — an open question, as Aczel\'s "I do not know" reflects. '
'ZP does not claim DC-freedom for the general case.',
bg=SLATE_LITE, border=SLATE
))
E.append(sp(6))
print('[build_zpj] Building Section VIII...')
E += [
hr(),
Paragraph('Section VIII: The Abstraction Chain — '
'ValuationStructure → AbstractSelfApp → AFAStructure', S['h1']),
hr(),
]
E.append(body(
'Developed in ZPJ_SelfApp.lean and ZPJ_Scale.lean after T-EXEC was established; '
'the abstraction chain reduces the axiom load of AFAStructure by deriving its fields '
'from a minimal fixed-point structure.',
style='bodyI'))
E.append(sp(4))
E.append(Paragraph('I. The Question: Can AFAStructure\'s Fields Be Derived?', S['h2']))
E.append(body(
'AFAStructure has three fields: selfMem (a predicate), quine_unique (AFA uniqueness), '
'and bot_self_mem (the bridge). These appear as structural prerequisites — '
'typeclass fields rather than freestanding axioms, but still commitments that any '
'instance must discharge. The abstraction chain asks: can these three commitments '
'themselves be derived from something more primitive?'))
E.append(body(
'The answer is yes, in two steps. First, AbstractSelfApp provides a self-application '
'operation and proves unique_fp, from which all three AFAStructure fields become '
'derived theorems. Then ValuationStructure explains why ⊥ is the unique '
'fixed point, making even unique_fp a theorem rather than a field.'))
E.append(Paragraph('II. AbstractSelfApp — The Minimal Fixed-Point Structure', S['h2']))
E.append(body(
'AbstractSelfApp encodes the abstract pattern common to both the set-theoretic and '
'2-adic domains: a self-application operation whose unique fixed point is ⊥.'))
E.append(def_box(
'AbstractSelfApp Typeclass (ZPJ_SelfApp.lean § I)',
[
'class AbstractSelfApp (L : Type*) [ZPSemilattice L] with:',
'(1) selfApp : L → L — the self-application operation.',
'(2) fixed_bot : selfApp(⊥) = ⊥ — ⊥ is a fixed point.',
'(3) unique_fp : ∀ x : L, selfApp(x) = x → x = ⊥ '
'— ⊥ is the ONLY fixed point.',
]
))
E.append(sp(6))
E.append(body(
'From these two fields, all three AFAStructure fields become derived theorems:'))
E.append(result_box(
'Derived Results from AbstractSelfApp (ZPJ_SelfApp.lean § II–III)',
[
'selfMemDerived x := selfApp(x) = x — self-containment as fixed-point property.',
'derived_bot_self_mem: selfMemDerived(⊥) — from fixed_bot. ✓',
'derived_quine_unique: any two self-containing elements are equal — '
'each equals ⊥ by unique_fp, so equal to each other. ✓',
'selfMem_eq_singleton_bot: {x | selfMemDerived(x)} = {⊥} — '
'via singleton_from_unique_witness. DC-free. ✓',
'instance toAFAStructure: any AbstractSelfApp gives an AFAStructure. '
'All three fields are theorems, not additional commitments. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('III. ValuationStructure — Why ⊥ is the Unique Fixed Point', S['h2']))
E.append(body(
'AbstractSelfApp assumes unique_fp. ValuationStructure derives it. The key insight '
'is the 2-adic argument: if scale increases valuation by 1 at every non-⊥ element, '
'then scale(x) = x implies val(x) = val(x) + 1 — impossible for any finite '
'valuation. Only ⊥, which has infinite valuation (val(⊥) = ⊤), '
'can be a fixed point.'))
E.append(def_box(
'ValuationStructure Typeclass (ZPJ_Scale.lean § I)',
[
'class ValuationStructure (L : Type*) [ZPSemilattice L] with:',
'(1) scale : L → L — the self-application (scaling) operation.',
'(2) val : L → ℕ∞ — valuation into the extended naturals.',
'(3) scale_bot : scale(⊥) = ⊥ — ⊥ is a fixed point of scale.',
'(4) val_bot : val(⊥) = ⊤ — ⊥ has infinite valuation.',
'(5) val_unique : ∀ x, val(x) = ⊤ → x = ⊥ '
'— only ⊥ has infinite valuation.',
'(6) val_scale : ∀ x ≠ ⊥, val(scale(x)) = val(x) + 1 '
'— scale strictly increases valuation at non-⊥ elements.',
]
))
E.append(sp(6))
E.append(result_box(
'Derived Results from ValuationStructure (ZPJ_Scale.lean § II–IV)',
[
'val_finite_of_ne_bot: x ≠ ⊥ ⇒ val(x) ≠ ⊤ '
'— contrapositive of val_unique. ✓',
'scale_ne_fixed: x ≠ ⊥ ⇒ scale(x) ≠ x '
'— val(scale(x)) = val(x) + 1 ≠ val(x) since val(x) is finite. ✓',
'scale_unique_fp: scale(x) = x ⇒ x = ⊥ — from scale_ne_fixed. ✓',
'instance toAbstractSelfApp: selfApp = scale; fixed_bot and unique_fp are theorems. '
'No additional fields. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('IV. The Full Chain and the 2-Adic Parallel', S['h2']))
E.append(body(
'The complete derivation chain is:'))
E.append(callout(
'ValuationStructure → AbstractSelfApp → AFAStructure\n'
'Four valuation axioms → Two fixed-point fields → Three AFA fields\n'
'At each step, the fields of the lower typeclass become derived theorems.',
bg=AMBER_LITE, border=AMBER
))
E.append(sp(6))
E.append(body(
'At each level of the chain, the 2-adic parallel holds. At the AbstractSelfApp level: '
'multiplication by 2 in ℚ₂ has 0 as its unique fixed point '
'(2x = x ⇒ x = 0, by ring arithmetic), and {x ∈ ℚ₂ | 2x = x} = {0} '
'by singleton_from_unique_witness. At the ValuationStructure level: in ℤ₂, '
'scale = ×2 and val = 2-adic valuation satisfy all four axioms — '
'in particular, v₂(2x) = v₂(x) + 1 for x ≠ 0 (proved from '
'PadicInt.valuation_mul and PadicInt.valuation_p in Mathlib). ℤ₂ cannot '
'be a formal instance because it is a ring, not a ZPSemilattice; the parallel is '
'proved as standalone theorems demonstrating the same proof structure closes both cases.'))
E.append(sp(6))
print('[build_zpj] Building Section IX...')
E += [
hr(),
Paragraph('Section IX: Concrete Instances — '
'ℕ∞ and OntologicalStates', S['h1']),
hr(),
]
E.append(body(
'Developed in ZPJ_Model.lean and ZPJ_OntBridge.lean to ground the abstraction '
'chain in concrete types; OntologicalStates takes a shorter path because its '
'two-element structure cannot support val_scale.',
style='bodyI'))
E.append(sp(4))
E.append(Paragraph('I. ℕ∞ — The Canonical ValuationStructure Instance',
S['h2']))
E.append(body(
'ℕ∞ = WithTop ℕ (the extended naturals) carries a ZPSemilattice '
'with join = min and bot = ⊤ (the natural maximum). The ZP partial order reverses '
'ℕ∞\'s natural order: x ≤₅ₚ y iff min x y = y iff x ≥ y. '
'So ⊤ is the ZP-bottom (valuation ∞, unique fixed point) and 0 is the '
'ZP-maximum (fully constrained).'))
E.append(def_box(
'ℕ∞ Instances (ZPJ_Model.lean)',
[
'instNatInfZPS: ZPSemilattice ℕ∞ with join = min, bot = ⊤. '
'A1–A3: min is associative, commutative, idempotent. '
'A4: min ⊤ x = x because ⊤ is the maximum. ✓',
'instNatInfVal: ValuationStructure ℕ∞ with scale = (· + 1), val = id. '
'scale_bot: ⊤ + 1 = ⊤ (WithTop.top_add). '
'val_bot: id ⊤ = ⊤. '
'val_unique: id x = ⊤ ⇒ x = ⊤. '
'val_scale: x ≠ ⊤ ⇒ id(x + 1) = id(x) + 1 (rfl). ✓',
]
))
E.append(sp(6))
E.append(result_box(
'Derived AFA Content on ℕ∞ (ZPJ_Model.lean § III)',
[
'natInf_scale_unique_fp: x + 1 = x ⇒ x = ⊤. '
'(The unique fixed point of (· + 1) in ℕ∞ is ⊤.) ✓',
'natInf_selfMem_singleton: {x : ℕ∞ | x + 1 = x} = {⊤}. ✓',
'Via toAbstractSelfApp and toAFAStructure, ℕ∞ carries a full AFAStructure '
'with all three fields as theorems. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('II. OntologicalStates — The Direct AbstractSelfApp Path',
S['h2']))
E.append(body(
'OntologicalStates = {null, exist} (ZP-B\'s two-element state space) cannot follow the '
'ValuationStructure path: a finite two-element type has no room for val_scale '
'(val(scale x) = val(x) + 1 would require infinitely many distinct values). '
'Instead it takes the direct path to AbstractSelfApp.'))
E.append(body(
'The self-application operation is the constant-to-null function: every element maps '
'to null. null is the unique fixed point because null ↦ null (fixed_bot) and '
'exist ↦ null ≠ exist (unique_fp holds vacuously for exist). '
'AFA content follows immediately from the AbstractSelfApp instance.'))
E.append(def_box(
'OntologicalStates Instances (ZPJ_OntBridge.lean)',
[
'instOntZPS: ZPSemilattice OntologicalStates with null-identity join and bot = null. '
'All four axioms proved by case analysis. ✓',
'instOntSelfApp: AbstractSelfApp OntologicalStates with selfApp = constant-to-null. '
'fixed_bot: null ↦ null = null (rfl). '
'unique_fp: null ↦ rfl; exist ↦ absurd hx (by decide). ✓',
]
))
E.append(sp(6))
E.append(result_box(
'Derived AFA Content on OntologicalStates (ZPJ_OntBridge.lean § III)',
[
'ont_bot_self_mem: null is self-containing. ✓',
'ont_quine_unique: any two self-containing elements of OntologicalStates are equal. ✓',
'ont_selfMem_singleton: {x | selfMemDerived(x)} = {null}. DC-free. ✓',
]
))
E.append(sp(6))
E.append(callout(
'Two concrete instances, two paths through the chain. ℕ∞ takes the full '
'ValuationStructure route. OntologicalStates bypasses ValuationStructure and connects '
'directly to AbstractSelfApp. Both deliver the same conclusion: the unique self-containing '
'element is the bottom. The architecture is sound because each type takes the path '
'the mathematics allows.',
bg=SLATE_LITE, border=SLATE
))
E.append(sp(6))
print('[build_zpj] Building Section X...')
E += [
hr(),
Paragraph('Section X: APG Decoration Uniqueness', S['h1']),
hr(),
]
E.append(body(
'Formalised in ZPJ_APG.lean as the most recent addition; this section proves the '
'full AFA decoration uniqueness theorem for finite accessible pointed graphs, '
'using the typeclass chain established in Sections VIII–IX.',
style='bodyI'))
E.append(sp(4))
E.append(Paragraph('I. Accessible Pointed Graphs and Decorations', S['h2']))
E.append(body(
'An Accessible Pointed Graph (APG) is a directed graph (Quiver) with a distinguished '
'root vertex from which every vertex is reachable via directed paths. AFA\'s central '
'theorem states that every APG has a unique set-theoretic decoration — a labelling '
'of vertices by sets satisfying the membership equation d(v) = {d(w) | v → w}.'))
E.append(body(
'ZP-J\'s version of this theorem is stated for an abstract DecorationUniverse rather '
'than sets. This avoids ZFSet (which satisfies Foundation, making self-loops impossible) '
'and places the result in the typeclass framework established above.'))
E.append(def_box(
'DecorationUniverse Typeclass (ZPJ_APG.lean § II)',
[
'class DecorationUniverse (U : Type*) [ZPSemilattice U] [ValuationStructure U] with:',
'(1) collect_singleton : collect {x} = scale(x) '
'— a singleton set decorates to scale of its element.',
'(2) collect_ext : collect s₁ = collect s₂ when s₁ = s₂ '
'— collect respects set equality.',
'(3) collect_val_ge : val(collect s) ≥ val(x) + 1 for x ∈ s and x ≠ ⊥ '
'— valuation of a collected set is strictly bounded below.',
'A valid decoration d : V → U satisfies d(v) = collect({d(w) | v → w}) '
'at every vertex v.',
]
))
E.append(sp(6))
E.append(Paragraph('II. The Valuation Argument for Cyclic Vertices', S['h2']))
E.append(body(
'The first key results handle cyclic vertices. If a vertex v lies on a directed cycle '
'of length k, then composing the decoration equation around the cycle gives '
'd(v) = scaleᵏ(d(v)). The valuation argument then forces d(v) = ⊥: '
'if d(v) ≠ ⊥, then val(scaleᵏ(d(v))) = val(d(v)) + k ≠ val(d(v)), '
'contradicting d(v) = scaleᵏ(d(v)).'))
E.append(result_box(
'Cyclic Vertex Theorems (ZPJ_APG.lean §§ III–VII\')',
[
'val_iterate: val(scaleᵏ(x)) = val(x) + k for x ≠ ⊥. ✓',
'scale_iterate_unique_fp: scaleᵏ(x) = x ⇒ x = ⊥ for k ≥ 1. ✓',
'pureSelfLoop_decoration_eq_bot: any valid decoration assigns ⊥ to a pure '
'self-loop vertex. ✓',
'kCycle_node_eq_bot: if d(v) = scaleᵏ(d(v)) under any valid decoration, '
'then d(v) = ⊥. ✓',
'cyclic_decoration_eq_bot: any vertex with a directed cycle through itself '
'receives ⊥ under any valid decoration. ✓',
]
))
E.append(sp(6))
E.append(Paragraph('III. The Acyclic Case and the "Infinite Period"', S['h2']))
E.append(body(
'Cyclic vertices have a finite period k — the path returns in k steps, and the '
'valuation argument closes the equation. Acyclic vertices have an "infinite period" — '
'the path never returns, so there is no cycle length k to close the equation. This is '
'the same zero-versus-infinity identification that runs throughout the framework: the '
'finite k of a cycle is the zero side; its absence is the infinity side.'))
E.append(body(
'The hardness of the acyclic proof is that "infinite period" gives you nothing to induct '
'on. Reach cardinality — the cardinality of {w | Path v w}, the set of '
'vertices reachable from v — serves as a finite proxy. For any child w of an '
'acyclic vertex v, the reach of w is a strict subset of the reach of v (since v cannot '
'be reached from w without creating a cycle). Reach cardinality is therefore strictly '
'decreasing, providing a well-founded measure for the induction.'))
E.append(result_box(
'Acyclic Induction and Global Uniqueness (ZPJ_APG.lean §§ VIII–IX)',
[
'acyclic_induction_step: if two valid decorations d₁, d₂ agree on all '
'children of an acyclic vertex v, they agree on v. '
'(From collect_ext applied to the decoration equations.) ✓',
'decoration_unique [Fintype V]: for any finite APG with root r and any two valid '
'decorations d₁, d₂ into any DecorationUniverse, d₁ = d₂. '
'Proof: strong induction on |{w | Path u w}|; cyclic case by cyclic_decoration_eq_bot; '
'acyclic case by acyclic_induction_step with IH on children. ✓',
]
))
E.append(sp(6))
E.append(callout(
'decoration_unique is the ZP version of AFA\'s decoration uniqueness theorem: for any '
'finite APG, at most one valid decoration exists into any DecorationUniverse. '
'The proof uses only the three typeclass axioms and ValuationStructure — it '
'characterises when decoration uniqueness holds. It does not construct a specific AFA '
'model or derive AFA\'s axioms from ZP\'s.',
bg=AMBER_LITE, border=AMBER
))
E.append(sp(6))
print('[build_zpj] Building registers...')
E += [hr(), Paragraph('Traceability Register — ZP-J', S['h1'])]
trace_rows = [
['T-EXEC: Quine atom = ⊥',
'AFAStructure.quine_unique + AFAStructure.bot_self_mem',
'None — typeclass fields',
'Lean: t_exec — axiom-free ✓'],
['J1: Quine join-identity',
'T-EXEC + ZP-A A4 (bot_join)',
'None',
'Lean: j1_quine_join_identity — axiom-free ✓ (was axiom ax_j1 in stub)'],
['CC-1 (Derived): S₀ = Q ⇒ S₀ = ⊥',
'T-EXEC',
'None',
'Lean: cc1_derived — axiom-free ✓ (was ZP-A conditional claim)'],
['bot_is_quine_atom',
'AFAStructure.bot_self_mem + quine_unique',
'None',
'Lean: bot_is_quine_atom — axiom-free ✓'],
['t_exec_iff: IsQuineAtom ↔ = ⊥',
'T-EXEC + bot_is_quine_atom',
'None',
'Lean: t_exec_iff — axiom-free ✓'],
['bot_unique: join-identity is unique',
'ZPE.da2_bottom_characterization',
'None',
'Lean: bot_unique — axiom-free ✓ (no AFA required)'],
['J_self = {⊥} (DC-free)',
'AFAStructure.quine_unique — one step',
'None',
'Lean: J_self_eq_singleton_bot — no Classical.choice ✓'],
['singleton_from_unique_witness',
'Set extensionality (propext)',
'None',
'Lean: singleton_from_unique_witness — axiom-free ✓'],
['AbstractSelfApp → AFAStructure',
'AbstractSelfApp.fixed_bot + unique_fp',
'None',
'Lean: toAFAStructure instance — all fields as theorems ✓'],
['ValuationStructure → AbstractSelfApp',
'ValuationStructure.val_scale + val_unique',
'None',
'Lean: scale_unique_fp, toAbstractSelfApp — axiom-free ✓'],
['ℕ∞ : ValuationStructure',
'ℕ∞ arithmetic (WithTop.top_add)',
'None',
'Lean: instNatInfZPS, instNatInfVal — axiom-free ✓'],
['OntologicalStates : AbstractSelfApp',
'Constant-to-null map; two-element case analysis',
'None',
'Lean: instOntSelfApp — axiom-free ✓'],
['cyclic_decoration_eq_bot',
'val_iterate + scale_iterate_unique_fp',
'None',
'Lean: cyclic_decoration_eq_bot — axiom-free ✓'],
['decoration_unique [Fintype V]',
'cyclic_decoration_eq_bot + acyclic_induction_step + Set.ncard',
'[Fintype V] — finite graph assumption',
'Lean: decoration_unique — propext, Classical.choice, Quot.sound ✓'],
['AFAStructure.bot_self_mem',
'AFA (ZF+AFA) — ⊥ = {⊥}',
'Typeclass field — proof obligation at instantiation',
'Not a theorem; a structural prerequisite.'],
]
E.append(data_table(
['Claim', 'Grounded In', 'New assumption?', 'Status'],
trace_rows,
[TW*0.22, TW*0.27, TW*0.22, TW*0.29]
))
E.append(sp(8))
E += [hr(), Paragraph('Open Items Register — ZP-J', S['h1'])]
oq_rows = [
['CC-1 (ZP-A) derivability',
'CLOSED — T-EXEC (ZP-J v1.0)',
'CC-1 is now a theorem. The Quine atom = ⊥ is structurally derived. '
'No freestanding axiom. No modelling commitment beyond AFAStructure typeclass fields.'],
['AX-J1 bridge axiom',
'CLOSED — J1 derived (v1.0)',
'The stub version had ax_j1 as a freestanding axiom. '
'The final version derives J1 from T-EXEC + ZP-A A4. Axiom eliminated.'],
['AFAStructure concrete instances',
'CLOSED — multiple instances',
'MachinePhase (ZP-K): machinePhaseAFA : AFAStructure MachinePhase. '
'ℕ∞ (v2.0): instNatInfZPS + instNatInfVal → AbstractSelfApp → AFA content. '
'OntologicalStates (v2.0): instOntSelfApp → AFA content directly.'],
['Aczel DC question (self-membership)',
'CLOSED — DC-free (v2.0)',
'For the self-membership operator, DC is unnecessary. '
'J_self = {⊥} proved in one step via quine_unique. '
'General set-continuous operators: still open (Aczel\'s "I do not know" stands).'],
['DA-1 Path 1 formalisation',
'PARTIAL — APG case proved (v2.0)',
'DA-1 Path 1 (ZP-E) invokes ⊥ = {⊥} informally. ZP-J T-EXEC formalises '
'the identification. decoration_unique (§ X) proves uniqueness for finite APGs '
'over abstract DecorationUniverses. The full ZF+AFA set-theoretic bridge '
'— showing the ZP types literally satisfy the ZF+AFA axioms — '
'remains outside Lean scope.'],
['ZP-A CC-1 label update',
'OPEN — editorial',
'ZP-A still labels CC-1 as a Conditional Claim. With T-EXEC established, '
'the label can be updated to Derived Theorem (citing ZP-J T-EXEC). '
'Mathematical content unchanged; editorial update only.'],
['Formal ZPSemilattice instance for a ValuationStructure type',
'OPEN — gap in chain',
'ZPJ_Scale.lean proves the ValuationStructure → AbstractSelfApp chain abstractly. '
'Connecting a concrete type (e.g. a 2-adic type or ZP state space) to both '
'ZPSemilattice and ValuationStructure in the same instance requires a bridge file '
'importing ZP-A and ZP-B. The ℕ∞ instance (ZPJ_Model.lean) fills this for '
'the abstract model; a concrete ZP-grounded instance remains future work.'],
]
E.append(data_table(
['Item', 'Status', 'Description'],
oq_rows,
[TW*0.22, TW*0.18, TW*0.60]
))
E += [
sp(12),
hr(),
Paragraph(
'End of ZP-J | Theorem T-EXEC: Executability of Self-Reference | '
'CC-1 derived — no freestanding axioms | '
'DC-free: J_self = {⊥} without Dependent Choice | '
'Abstraction chain: ValuationStructure → AbstractSelfApp → AFAStructure | '
'Instances: ℕ∞, OntologicalStates | '
'decoration_unique: any two valid decorations of a finite APG agree | '
'All results sorry-free in Lean 4',
S['endnote']),
]
print(f'[build_zpj] Calling doc.build() with {len(E)} elements...')
doc.build(E)
print(f'[build_zpj] Written: {out_path}')
if __name__ == '__main__':
build()