A Lean 4 formalization: one diagonal fixed point at the bottom of five mathematical fields - the snap off it a theorem, the recurrence machine-verified, the boundary proved.
Code: Apache License, Version 2.0. Documents (the PDFs, the site layouts, and every Markdown file except CLAUDE.md and those under tools/ and .claude/): CC BY-NC-ND 4.0. Third-party material keeps its own licence. See NOTICE.
- Start here (the shortest path) - The Minimal Core: the whole shape the framework is built on - engine, wall, floor, the snap in both directions, the fan-out - in one self-contained Lean file, on the smallest objects that can carry it, checkable in one command. The compact front door for either a mathematician or a general reader.
- General reader - Guide: plain language, illustrated companions, and reading paths for every audience.
- Mathematician or reviewer - the formal index is below: Lean verification, the document table, and the reading order by specialty. Claim-by-claim status, with Lean witnesses and exact axiom profiles, is in the Claims Ledger.
- Just want the object - The Bottom Element (⊥) and The Binary Snap (⊥ → ε₀): dictionaries and maps of ⊥ and the transition off it, most characterizations carrying a machine-checked Lean witness.
The same family of objects sits at the bottom of every framework it touches. In order theory, p-adic valuation, category theory, computability, and set theory, each domain's bottom element ⊥ is the same kind of thing: a diagonal fixed point - the point that is its own image under the domain's self-map. This project machine-verifies that recurrence and proves exactly how far it reaches.
That the classical self-reference arguments share one diagonal fixed point is prior art, not this framework's: Lawvere (1969) for Cantor, Russell, Gödel and Tarski, Yanofsky (2003) for Turing and the recursion theorem. What this framework adds is checkable and specific:
- It is located at the floor, not the ceiling - the Gödel inversion. The concrete instance, the Binary Snap (⊥ → ε₀), is a theorem, not an axiom; the core snap
t_snap_derivedis Lean-kernel-axiom-free - not even choice. Choice enters elsewhere in the framework, including at the separate identification of that first step with the ordinal ε₀; see The Result below for where. - The recurrence is verified across heterogeneous domains - the computability face is a machine-checked Kleene/Rogers fixed point, and a Lawvere-form instance in multi-valued form (cited: Bauer 2017); the lattice and 2-adic faces are proved fixed points of their own self-maps (
q2_unique_fp,scale_unique_fp), carrying the shape but not genuine Lawvere instances - Cantor forbids the Set-level witness. - The boundary is proved, not assumed - there is no single cross-category theorem folding the domains into one object (
x = yacross distinct categories is not a well-formed proposition); a Cantor/Lawvere obstruction establishes the impossibility. The framework proves where the shape recurs, and where it stops.
The transition ⊥ → ε₀ - the Binary Snap, this project's shorthand - is a theorem, not an axiom. The existence of an atom above ⊥ of the discrete state chart (a state with nothing between it and ⊥; c₁ in MachinePhase) - what the framework calls a first atomic state - does not follow from A4 alone: a join-semilattice with a least element can be densely ordered and atomless, and a densely ordered set has no first step anywhere (Mathlib's denselyOrdered_iff_forall_not_covBy, restated as axb1_fails_everywhere_iff_dense), so ℝ≥0 under max, whose least element is 0, has none. What supplies the atom is the framework's discrete state model - the states are atomic, not a continuum (AX-B1) - with A4 (∀ x, ⊥ ∨ x = x) giving only the join structure of the transition. The assembly is machine-verified in Lean 4 (t_snap_derived). The framework adds no snap-specific axiom (AX-1 is retired: the shape of the snap is proved, as Theorem T-SNAP, and that the snap occurs is stated separately: it follows from the occurrence commitment, that instantiation occurs, together with DA-1, closed given DP-2), and t_snap_derived - the snap from ⊥ of MachinePhase to its atom c₁ - depends on no Lean axioms at all (#print axioms is empty): not the Axiom of Choice, not even propositional extensionality (the discreteness is carried by the finite state type and checked constructively, not invoked as a classical axiom). Identifying that first step with the proof-theoretic ordinal ε₀ is a separate step, and that is where Classical.choice enters - as it does at many of the places the framework builds on Mathlib's classically-built analysis, order, and computability libraries (p-adic topology, Hilbert space, ordinals), though not at all of them, and never in the core snap itself. Not all of them: IsKleeneFixedPoint, whose type is eval c = f c over Mathlib's Nat.Partrec.Code, measures axiom-free, and ZP-K Section IV holds a dated measurement table of which declarations carry it - it is meant to be re-run, not cited. Some of the choice is the framework's own; ChoiceCannotBe.lean § IV collects cases among them whose principles reduce to a taboo, with those reductions. The category-theory face is one example: its choice is a bare classical in Lawvere.lean, and it is essential rather than incidental, given the premise stated in § IV - a separate axis from where the choice comes from - since wem_of_fixedPointFree reduces the general fixed-point-free principle to weak excluded middle. The honest contrast, showing exactly where choice appears, is a checkable artifact: AxiomProfile.lean.
The transition's destination and form are forced - each by a mechanism with its own requirement and its own Lean witness. That it OCCURS follows from the occurrence commitment (instantiation occurs) together with DA-1 (closed given DP-2) (see the closing note below):
- Information - ⊥ is the degenerate distribution (a point mass, zero information); a non-degenerate state provably needs at least two outcomes, so the minimal non-⊥ structure is binary, with no "half state." Requires: states are probability distributions. Witnesses:
pmf_subsingleton_isPure(fewer than two outcomes forces the point mass),binaryState_exhaustive(no third state, axiom-free); the two point masses are exactly 1 bit apart (t1b_jsd). - Order - given two distinct states, the transition from ⊥ to an atom above it (c₀ → c₁ in
MachinePhase) is a join. Requires: the bottom-element axiom A4. Witness:t_snap_derived. - Self-execution - nothing external can execute ⊥ of a ZPSemilattice, the occupant of the framework's ⊥ role, so if it executes at all, the executor is that ⊥ itself, and execution is a state change off ⊥ of
MachinePhase. That rules out an external executor, not an inert ⊥. Requires: that ⊥ admits no external interpreter; that the configuration reaching the incompressibility threshold P₀ is executing is the occurrence commitment, not a consequence, and DA-1 consumes it and does not supply it. Witness (structural half only):da1_closed_concreteprovesIsQuineAtom (bot : MachinePhase)- it mentions no code and no execution. - Incompressibility - the surprisal I(n) = n at ball-hierarchy depth n is unbounded: every bound M is exceeded at some depth. Requires: the information measure. Witness:
l_inf. Reading: ZP-C models its state c₀ as corresponding to the ⊥ of its configuration semilattice (CC-2, a modelling commitment), and reads c₀ as corresponding to the limit point 0 of the binary ball hierarchy at infinite depth (a reading across carriers, MC-1), and read there c₀ has no finite description; l_inf itself is a statement about depth n. This is what motivates the self-execution reading - a state without a finite description cannot be held by any external interpreter - and the step from unbounded surprisal to executing is a bridge principle of its own, which the framework does not adopt and which is not the occurrence commitment (ZP-E, DA-1 Path 2).
These force different aspects, not the same proposition four times: incompressibility is what motivates the self-execution reading; the information mechanism fixes its destination as the minimal binary state; and A4 gives it a join form. Together they constrain every aspect of ⊥ → first-atomic-state except that it fires, which follows from the occurrence commitment (instantiation occurs) together with DA-1 (closed given DP-2). The single substantive commitment underneath is that states are discrete - a state exists or it does not, a distribution over atomic outcomes, not a continuum - which is exactly what the reals lack, and why the snap provably fails there (f_snap_impossible).
The bottoms across the layers form one characterized family (MC-1): per-domain membership is proved (the categorical criterion is mc1_correspondence), while the reading that they are numerically one object is retired as ill-typed (object equality across categories does not typecheck and is not invariant under equivalence); what separates the members is proved property by property (seam_unique_among_named, for the named bottoms, in a lattice with no top). ε₀ is chosen as the proof-theoretic ordinal of PA - a cited classical fact the framework invokes, not one it re-proves, and it takes more than one result: transfinite induction up to ε₀ suffices to prove the consistency of PA (Gentzen, Math. Annalen 112 (1936) 493-565); that induction is not itself provable in PA, which follows indirectly from Gödel's theorem together with the 1936 result and which Gentzen proved directly in Math. Annalen 119 (1943) 140-161; and transfinite induction up to any ordinal strictly below ε₀ is provable in PA, which Gentzen reports as already known, crediting Hilbert-Bernays. What pins the value to exactly ε₀ is the last two of those together, and they run in opposite directions: PA proves transfinite induction at every ordinal strictly below ε₀, and does not prove it at ε₀ itself. Its role as the exact snap threshold is machine-verified. The type-level identity across types is ill-typed, not open: an identity between a MachinePhase state and an ordinal is not a well-formed statement, the same category error as an identity across Ordinal and ℤ₂, which fails to elaborate (cnf_bridge_type_boundary co-witnesses the two limits instead), and the formal link runs through maps (the threshold map α ↦ if α < ε₀ then c₀ else c₁, the witness of c1_epsilon_zero_identification, order-non-decreasing by snap_map_mono; snapEmbed). The full labelled account is in Axiomatic Commitments.
The snap is also irreversible: the p-adic topology layer (ZP-B) establishes, Lean-verified, that there is no continuous path from any nonzero element of Q₂ back to 0 (c3_irreversible) - the total disconnectedness of Q₂ makes any return path discontinuous. This is a claim about the carrier rather than about the snap alone - it holds in Q₂ and fails in ℝ, which is connected (Statement: CARRIER, this project's label for a property that holds in one carrier and fails in another).
Scope of the claim. The internal coherence is formally established - the central theorem and the supporting layer theorems are verified in Lean 4 given the explicitly stated commitments. Whether those commitments are the right ones, and whether the formalism faithfully tracks the structural notion of zero it sets out to model, are questions Lean cannot answer from inside; they are what this repository invites external review on. The framework has been developed in public from the start for exactly this reason.
The derivation chain - the step-by-step formal skeleton - click to expand
P₀ (incompressibility threshold, ZP-C D1)
→ the occurrence commitment (the configuration reaching P₀ is a running machine's current configuration, not an inert string, ZP-E; a commitment, not derived)
→ D7 (machine configuration definition, ZP-C; given the occurrence commitment, a running machine has left c₀ for c₁)
→ DA-1 (DP-2 and da1_minimal_path show c₀ and c₁ distinct while returning the same output value, ZP-E; closed given DP-2; it consumes the occurrence commitment and does not supply it)
→ L-RUN (execution is a state change off ⊥ of MachinePhase, c₀ ≠ c₁, ZP-C)
→ TQ-IH (c₁ ≠ c₀: the same fact read from c₁, ZP-C)
→ ZP-A D2 (a state change off ⊥ of MachinePhase is a join - the Binary Snap)
→ T-SNAP (Binary Snap derived: A4, the standard bottom element axiom, gives its join, AX-B1 supplies the atom, and t_snap_given takes the start at ⊥ and occurrence at the first step as hypotheses; AX-1 is retired: the snap's shape is this theorem, and that the snap occurs is stated separately: it follows from the occurrence commitment, that instantiation occurs, together with DA-1, closed given DP-2)
Machine-checked proofs of the formal documents using Lean 4 + Mathlib, with source under ZeroParadox/ in this repository. Every push and pull request to main is re-verified from scratch by a continuous-integration build that runs the full lake build, so the published state is always one that compiles. An axiom-profile artifact, AxiomProfile.lean, collects the axiom dependencies of the core results in one place: the central theorem T-SNAP depends on no axioms, the choice-free core (lattice, Quine-atom self-reference) is listed, and an honest contrast shows where Classical.choice enters (the analytic realizations). The full claim-by-claim status - every result with its Lean witness and exact axiom footprint, the by-document verification table, and the per-file axiom profile - is in the Claims Ledger.
Browse the source tree: the full Lean sources are navigable on GitHub at ZeroParadox/ (GitHub renders each file with syntax highlighting and provides the directory listing); individual files also resolve directly under ZeroParadox/ on this site.
The checks on the prose are published too. Beyond the Lean build, this repository gates its own writing: a set of deterministic checkers in tools/verify/ refuses a commit or a push that adds an unmeasured modal claim, an undated artifact count, a point-of-view claim with no declared kind, a requirements class with no degeneracy verdict, or a prose block over its cap. python tools/verify/ci_report.py runs the suite and prints what passed, what is grandfathered debt, and what was skipped. ⚠ The checkers gate a commit and a push through git hooks, which git cannot version-control - a fresh clone has none until python tools/verify/install_hooks.py installs them, and --check reports whether they are armed. The review briefs the human-judgement gates are run from are in .claude/commands/. ⚠ Those briefs are readable but not runnable from a clone: they reference a private working folder (.claude-local/) holding session notes, correspondence and the defect ledger, and four of them hand you commands that live there. The method is public; some of the material it operates on is not, and that is stated here rather than left to be discovered. Neither is needed to build the Lean sources or the documents - they are published so the "check it yourself" claim covers the writing as well as the mathematics.
An independent re-check is three commands: git clone https://github.com/timbrigham/ZeroParadox && cd ZeroParadox && lake build. elan reads the pinned compiler from lean-toolchain (leanprover/lean4:v4.30.0-rc2) automatically, and Mathlib is fetched as a pinned dependency via lake-manifest.json; a clean lake build means every theorem in ZeroParadox/ type-checks against the Lean kernel. To inspect the core axiom profile directly: lake env lean ZeroParadox/AxiomProfile.lean.
| File | Document | Version | Focus |
|---|---|---|---|
| Lattice Algebra | ZP-A | v1.33 | The lattice-algebra foundation: the bottom element ⊥ and the order it induces. |
| p-adic Topology | ZP-B | v1.30 | The 2-adic topology: why p = 2, and why departure from ⊥ is irreversible. |
| Information Theory | ZP-C | v1.26 | The information layer: state distributions, 1-bit cost, unbounded surprisal at ⊥. |
| State Layer | ZP-D | v1.19 | The Hilbert-space layer: the snap as an orthogonal shift between states. |
| Bridge Document | ZP-E | v3.61 | The bridge: the snap assembled as a derived theorem across the layers. |
| The Counterexamples | ZP-F | v1.20 | The counterexamples: ordered fields (ℝ, ℚ) where the snap cannot occur. |
| Category Theory | ZP-G | v1.23 | The categorical layer: ⊥ as initial object, the informational singularity. |
| Categorical Bridge | ZP-H | v1.27 | The categorical bridge: the snap holding under all four domain functors. |
| Native Categories Addendum | ZP-H Native Categories Addendum | v1.7 | The snap floor realized inside each framework's native Mathlib category (TopCat, ModuleCat ℂ, KleisliCat PMF). Reads after ZP-H. |
| Inside Zero | ZP-I | v1.28 | Inside zero: each nowhere-zero 2-adic sequence whose valuation equals a depth index in ℕ that climbs at every step converges to 0 in the 2-adics; reading that limit as an occupant of the ⊥ role, and then as a successor ⊥′, are two further commitments. |
| Self-Reference | ZP-J | v2.13 | Self-reference: ⊥ as the Quine atom, and the AFA structure it requires. |
| AFA Addendum | ZP-J AFA Addendum | v1.19 | Decoration uniqueness for finite graphs from the valuation structure alone. Reads after ZP-J. |
| Wheel Addendum | ZP-J Wheel Addendum | v1.8 | The wheel of fractions as a wheel: division by zero made total. Reads after ZP-J. |
| Keystone Addendum | ZP-J Keystone Addendum | v1.26 | The diagonal-fixed-point keystone: the Lawvere face-split (Set face machine-checked, computability face cited) and the snap as a well-foundedness boundary crossing. Reads after ZP-J. |
| Computational Grounding | ZP-K | v1.27 | Computational grounding: the bottom's structural self-containment, with the computational reading carried as a commitment. |
| Incomputability Convergence | ZP-L | v1.30 | ε₀ as the exact ordinal threshold the snap is keyed to. (That the snap occurs follows from the occurrence commitment together with DA-1, closed given DP-2.) |
| Kleene-Ordinal Bridge | ZP-M | v1.13 | The bridge between the Kleene quine and the ε₀ fixed point. |
| The Constructive Snap | ZP-N | v2.5 | The constructive companion to ZP-L: the ε₀ snap from below on ordinal notations, choice-free (propext only). Locates ZP-L's classical dependency in Mathlib's order instance, and proves that comparing arbitrary well-orders implies excluded middle (a known taboo, cited to Kraus/Nordvall Forsberg/Xu), so comparability has no choice-free proof given the premise stated in ChoiceCannotBe.lean § IV. Adds a carrier of notations denoting the ordinals up to ε₀, whose crossing into Ordinal is one named map with a measured price. ZP-L's ε₀ results, as stated, carry Classical.choice in their statements (measured 2026-10-08); the ascent below ε₀ is restated choice-free on ordinal notations, and for ε₀ itself a choice-free Lean restatement of the fixed-point equation and its uniqueness on E0Note sets existence by definition, while a choice-free derivation in Lean of the fixed point on a well-founded carrier, leastness included, was not located as of 2026-10-08 (SnapNucleus.md § Axiom footprint). |
| The Fixed-Point Fork | ZP-P | v1.26 | Synthesis layer: the least-vs-greatest fixed-point fork, generalizing the Foundation/AFA orthogonal-contact-point claim across frameworks. |
| The Frame-Change | ZP-Q | v1.13 | Synthesis layer (ZP-P sequel): the bottom read as both 0 and ∞, and what that does not settle. The order-theoretic frame-flip universal is proved; the categorical Lawvere universal meets a proven Cantor wall; the cross-domain identity is a type boundary. |
| Cross-Category Fixed Point | ZP-R | v1.20 | Synthesis / placement layer. The framework's self-application fixed point is a role filled per face: in the fork / AFA face by ⊥ of the ZPSemilattice, a fixed point and the only one by the class fields fixed_bot and unique_fp of AbstractSelfApp (selfApp_pinnable), not produced by Lawvere's engine; in the computability face by a Kleene code, with fixed points up to eval (Rogers' form), infinitely many for each partial computable F (fixed_points_infinite). It asks where the role is filled by a Lawvere fixed point across three faces: refuted in Set on every carrier except a one-element one (Cantor), free of a monotone obstruction on complete lattices (Knaster–Tarski), with no reflexive object built here and no map from the two-element chain onto its monotone self-maps (the first finite stage of Soto-Andrade and Varela's two-element example, 1984, §2.5, pp. 15–16; the case Y = 2 of Trimble's Cantor theorem for posets; Bergman 2008, Cor. 7), and realized in the computability face (Rogers/Kleene, the crossing; that Rogers' general form is a Lawvere instance is cited). F1 states what is measured per face; how the faces formalized here relate to Lawvere's theorem is collected in ZP-R Section III, in the box "Lawvere's theorem, face by face", and ZP-R conjectures nothing global. Outside the PDF, the narrower case of computable eval-respecting maps is checked in Lean (hasWitnessRel_evalClass with fixedPoint_of_witnessRel, ZeroParadox/Category/DiagonalWitness.lean). |
| Diagonal Family Addendum | ZP-R Diagonal Family Addendum | v1.18 | The faces formalized here of the self-referential relationship, by the μ/ν fork: wall faces (Cantor, Russell, Turing, Tarski, Curry) where self-reference cannot close, and floor faces (Quine atom, Kleene quine, Löb / Gödel 2nd, Rice) where it does, Löb / Gödel 2nd from a hypothesized Löb diagonal; Gödel's first incompleteness sits between the columns and is not formalized here. Lean-witnessed except the Gödel-first row. The self-application fixed point is a role filled per face: in the fork / AFA face by ⊥ of the ZPSemilattice, from the class fields (t_exec); in the computability face by a Kleene code, computability_face_fixedPoint giving every computable self-map on codes a fixed point up to eval (Rogers' form). Reads after ZP-R. |
| The Choice-Free Core | Choice-Free Core | v1.13 | Framework-wide note: the central results are choice-free (T-SNAP is axiom-free); the framework is not choice-free as a whole - most of its choice is inherited from Mathlib in the analytic realizations, and some is the framework's own. ChoiceCannotBe.lean § IV collects cases, of either provenance, where a general statement proved with choice implies excluded middle or its weak form by a choice-free reduction, and ZeroParadox/AxiomProfile.lean § 0 prints their footprints; for the fixed-point-free case this concerns the general statement over arbitrary types: restricted to carriers with decidable equality it is [propext] (fixedPointFree_of_nontrivial_decidable). See CLAIMS.md. Anchored on AxiomProfile.lean. |
The framework is not a line. Several fields each reach a bottom, and those bottoms all play the same structural role, the diagonal fixed point ⊥; the documents above are the spokes into it. Start at the hub, then follow your own field. A document that appears in more than one field's route is a bridge, and the overlap is the point: the fields' bottoms share one structural shape. Whether they are literally one object is a type boundary, not a theorem (see The Frame-Change).
Start here (the hub, for everyone): two companion maps - The Bottom Element (⊥), the map of the object ⊥, and The Binary Snap (⊥ → ε₀), the map of the transition off it - each with what is proved versus open → Bridge Document, the snap assembled as a derived theorem → The Frame-Change, the bottom read as both 0 and ∞, and why every field's bottom plays the same structural role. Keep the Claims Ledger beside you for proved-versus-conjectural status.
Then follow your field:
- Number theory and valuation (p-adic): p-adic Topology → The Counterexamples → The Frame-Change (the p-adic Riemann sphere)
- Proof theory and ordinals: Incomputability Convergence → Kleene-Ordinal Bridge → The Constructive Snap
- Computability and recursion: Computational Grounding → Kleene-Ordinal Bridge
- Set theory and foundations (AFA): Self-Reference, with the AFA and Keystone addenda → The Fixed-Point Fork
- Category theory: Category Theory → Categorical Bridge, with the Native Categories addendum → The Fixed-Point Fork and The Frame-Change
- Order, lattice, and state: Lattice Algebra → Inside Zero, then the state layers Information Theory and State Layer
Each spoke is the same three beats: your field, then the bridge that carries it out, then back to ⊥. Read your own layers, then the synthesis layer they feed (The Fixed-Point Fork or The Frame-Change), then the hub, and you will see your field's bottom is doing the same structural work as every other field's.
The spine (the argument itself, no field assumed): The Bottom Element (⊥) → Bridge Document → The Fixed-Point Fork → The Frame-Change → Cross-Category Fixed Point. This is the through-line, and it replaces the old single linear reading order, which tried to send every reader through all of the documents in one sequence.
Orientation and general readers: The Choice-Free Core records the axiom profile; the Foreword gives context; plain-language companions and a general-reader path are in Guide. The Wheel Addendum (division by zero made total) is a self-contained aside off the set-theory route.
This framework adds no axioms specific to the result: the central theorem takes its join from the standard bottom-element axiom of join-semilattice theory and its atom from AX-B1. Its start at ⊥ and occurrence at the first step are stated as hypotheses in t_snap_given, which binds no atom. AX-1 (Binary Snap Causality) is retired. Its content was split in two: the shape of the snap is proved, as Theorem T-SNAP, and that the snap occurs is stated separately: it follows from the occurrence commitment (instantiation occurs) together with DA-1 (closed given DP-2). tsnap_holds_but_nothing_moves shows T-SNAP does not carry it. T-SNAP is derived in ZP-E.
Of the remaining commitments, most are restatements of structure established in earlier layers (AX-G1's initial object is grounded in ZP-A's bottom element, and AX-G2 in ZP-A antisymmetry with ZP-B C3; AX-G1's no-terminal half is ZP-G's own commitment, since ZP-A's two-state carriers have a top). One is substantive and is not reducible to computation: AX-B1, that existence is discrete rather than a continuum of partial states. AX-B1 holds at every state with anything above it: each has a first distinct state above it, with nothing strictly between. A state with nothing above it owes no step. The decide proof (ax_b1_distinct) checks that the two states are distinct given a two-element type; choosing a discrete alphabet over a continuum is the commitment itself, and is not what decide verifies. See the Claims Ledger for the full statement.
The framework is stated over ZF + AFA (not ZFC), but the commitment is not the adoption of AFA specifically: it is a set of requirements on the host theory - that the bottom is a Quine atom (⊥ = {⊥}: its only member is itself, the reading CC-2 commits to), and that it is the only such reflexive set - of which AFA is the canonical example, since AFA allows at most one solution of x = {x} (Aczel 1988, p. 19). Those requirements are a checkable object, the QuineAtomHost typeclass (ZeroParadox/Settheory/QuineHost.lean): Foundation-freeness is forced by ⊥ ∈ ⊥ (quineAtomHost_not_wellFounded); ZFC + Foundation is excluded in-kernel about Mathlib's real ZFSet (zfSet_no_singleton_bottom); Boffa's BA₁ - its reflexive sets form a proper class, not one (Aczel 1988, Prop. 5.1, p. 57) - fails the uniqueness, witnessed by a toy model (boffa_fails_reflexive_unique) rather than an in-kernel fact about that theory; and AFA's pattern meets both requirements in a finite toy with real membership, a model of the pattern and not of AFA. The older class QuineHost, which asks for ⊥ ∈ ⊥ with no other self-membered element, is a different requirement: AFA's membership fails it, since 0* = {∅, 0*} is self-membered (Aczel 1988, Example 1.5, p. 7), and the two classes are incomparable (QuineHost.lean § VII). Only "these are the right requirements to demand" remains argued (and where AFA-specific results are used elsewhere, they are proved separately, not assumed from full AFA); the discipline every such claim must meet is defined in Forced Metatheoretic Commitment. The bottoms across the layers form one family (MC-1): per-domain membership is proved (its correspondence half is mc1_correspondence), and the reading that they are numerically one object is retired as ill-typed.
The full labelled account - the supporting commitments (AX-B1, AX-G1, AX-G2, MP-1, RP-1, DP-1), the metatheoretic stance and the host-theory requirements (where AFA fits), and the bottom-family (MC-1) account in full - is in the Claims Ledger (Tiers 4-5).
The framework's open questions, design commitments, and resolved questions are tracked in the Claims Ledger - Tier 6 (open: the Classical.choice necessity question, OQ-E2, the Lawvere conjecture), Tier 5 (chosen commitments), and the Resolved-questions list.
Verification status: ZP-A through ZP-N, ZP-P, ZP-Q, and ZP-R, plus the ZP-H native-category functors and mc1_correspondence, are machine-verified in Lean 4. A second-prover cross-check (e.g. Rocq) is not yet done.
Open questions are discussed publicly in the GitHub Discussions Open Questions category.
Hosted at timbrigham/ZeroParadox. Previous document versions are preserved in the repository's git history and in each release's Zenodo/DOI snapshot. See Guide for development notes and process documentation.
The code is licensed under the Apache License, Version 2.0: see LICENSE. The code is every file that is neither a document as defined below nor third-party material: the Lean files, the build scripts, everything under tools/ and .claude/ (the Markdown there included), CLAUDE.md, and the configuration files.
The documents are licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License (CC BY-NC-ND 4.0): see LICENSE-DOCS. The documents are the PDFs at the repository root, every Markdown file except CLAUDE.md and those under tools/ and .claude/ (this README included), and the site layouts in _layouts/. You may share them with attribution for non-commercial purposes only, and you may not share adapted versions.
Third-party material is covered by neither licence and keeps its own. The vendored Lean under ZeroParadox/Vendored/ and the port ZeroParadox/Ordinal/NaturalOpsPow.lean are under the Apache License, Version 2.0, from their original authors: ZeroParadox/Vendored/CorpusAudit/ carries its licence text beside it, and for the other two the text is the root LICENSE. The fonts in scripts/fonts/ carry their licence texts beside them: DejaVu is under the Bitstream Vera and Arev font licences, with the DejaVu changes in the public domain, and STIX Two is under the SIL Open Font License, Version 1.1. NOTICE states which paths fall under which licence.
If referencing this work, please cite:
Brigham, Timothy. The Zero Paradox (2026). https://github.com/timbrigham/ZeroParadox
For inquiries, discussion, or collaboration, reach out by email at timbrigham@zeroparadox.org or open an issue on GitHub.