The Zero Paradox

April 2026

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.

Followed a link that broke after the v3.0 source reorganization? The old→new file and declaration map is in ssot.json; report anything we missed in the v3.0 reorg link-integrity thread.

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 (Cantor, Russell, Gödel, Kleene) share one diagonal fixed point is Lawvere’s (1969). 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 (the forced exit ⊥ → ε₀), is a theorem, not an axiom; its core snap is even Lean-kernel-axiom-free (not even choice - choice enters only at the separate identification of the ceiling with the ordinal ε₀).
• The recurrence is verified across heterogeneous domains - the computability face is a genuine Lawvere/Kleene fixed point; 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 = y across 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.

Where to Start

• 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.
• General reader - Guide: plain language, illustrated companions, and reading paths for every audience.
• 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.
• See it - The Bottom Family: an interactive map of ⊥ across the fields - hover any node for why it sits where it does, with the Lean witness to check.

The Result

The forced transition ⊥ → ε₀ - the Binary Snap, this project’s shorthand - is a theorem, not an axiom. The existence of a minimum non-⊥ state is the atom above ⊥ - what the framework calls the first atomic state - and it does not follow from A4 alone: a bounded join-semilattice can be dense and atom-free (ℝ≥0 under max is one), and the framework proves the snap fails exactly there (f_snap_impossible). What supplies the atom is the framework’s discrete state model - the ontological 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 (the redundant AX-1 was retired), and t_snap_derived - the snap from ⊥ to the first atomic state - depends on no Lean kernel axioms at all: 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 ceiling with the proof-theoretic ordinal ε₀ is a separate step, and that is where Classical.choice enters - as it does wherever the framework builds on Mathlib’s classically-built analysis, order, and computability libraries (p-adic topology, Hilbert space, ordinals, category theory), never in the core snap itself. The honest contrast, showing exactly where choice appears, is a checkable artifact: AxiomProfile.lean.

Every part of the transition is forced - its occurrence, its destination, and its form - each by a mechanism with its own requirement and its own Lean witness:

• 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 ⊥ → first atomic state is a join. Requires: the bottom-element axiom A4. Witness: t_snap_derived.
• Self-execution - nothing external can execute ⊥, so ⊥ must execute itself, and execution is a non-null state change. Requires: ⊥ admits no external interpreter. Witness: da1_closed_concrete (⊥ is a Quine atom).
• Incompressibility - ⊥ has no finite description: its surprisal is unbounded. Requires: the information measure. Witness: l_inf. This is what grounds self-execution - a descriptionless ⊥ cannot be held by any external interpreter.

These force different aspects, not the same proposition four times: incompressibility grounds self-execution, so the snap must occur; the information mechanism fixes its destination as the minimal binary state; and A4 gives it a join form. Together they leave no part of ⊥ → first-atomic-state unforced. 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 - the members are provably distinct (the walls). ε₀ is chosen as the proof-theoretic ordinal of PA (Gentzen 1936) - a cited classical fact the framework invokes, not one it re-proves; its role as the exact snap threshold is machine-verified, and the one open residue is the type-level identity across universes (OQ-E2), not the Gentzen relationship itself. 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 state back to ⊥ - the total disconnectedness of Q₂ makes any return path discontinuous.

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 Framework

Formal Verification (Lean 4)

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.

Reproducing the Verification

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.

Formal Framework Documents

Reading Order (by Specialty)

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 snap read as a change of point of view 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 and The Philosophical Question give 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.

Axiomatic Commitments

This framework adds no axioms specific to the result: the central theorem follows from the standard bottom-element axiom of join-semilattice theory alone, and AX-1 (Binary Snap Causality) is no longer an axiom - it is Theorem T-SNAP, derived in ZP-E. The remaining commitments are either directly verifiable by computation or restatements of structure established in earlier layers.

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 self-containing Quine atom (⊥ = {⊥}), and that this atom is unique - of which AFA is the canonical example. Those requirements are a checkable object, the QuineHost typeclass (ZeroParadox/Settheory/QuineHost.lean): Foundation-freeness is forced by the Quine atom (quineHost_not_wellFounded); ZFC + Foundation is excluded in-kernel about Mathlib’s real ZFSet (zfSet_no_quine_bottom); Boffa’s permissiveness - it admits a proper class of Quine atoms, not one - is what fails (Z), witnessed by a toy model (boffa_fails_unique) rather than an in-kernel fact about that theory; and AFA satisfies all three (afaStructure_isQuineHost). 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).

Question Register

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.

Version History

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.

License

All conceptual development, structure, and authorship originate with the human creator.

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License (CC BY-NC-ND 4.0).

You may share the work with attribution, but you may not modify it or use it commercially. See License for full details.

Citation

If referencing this work, please cite:

Brigham, Timothy. The Zero Paradox (April 2026). https://github.com/timbrigham/ZeroParadox

Contact

For inquiries, discussion, or collaboration, reach out by email at timbrigham@zeroparadox.org or open an issue on GitHub.