Zero Paradox Claims Ledger

The bottom elements across the layers - the algebraic ⊥, the 0 of Q₂, the Turing initial configuration c₀, and the categorical initial object - form one family (MC-1), each a member characterized by shared criteria it satisfies - and all sharing the self-referential (diagonal) fixed-point shape. Membership splits into a correspondence half, now formally realized in Lean, and a former identity half - that the four are numerically one object - which is retired as ill-typed rather than held as a commitment (the members are provably distinct, the walls). Its faces are the Quine atom (⊥ = {⊥}) in set theory, the Kleene quine in computation, the point v₂(0) = ∞ in valuation, and the initial object in category theory. This identification is substantially grounded rather than stipulated: each domain locates its own bottom through its own logic first, and the cross-layer agreement is then enforced formally (the ZP-E typeclass instance ties ZP-A ⊥ to ZP-C c₀; AX-G1 grounds the categorical initial in ZP-A ⊥; ZP-H T-H3 proves snap consistency across all four functors). The categorical correspondence is now realized in the standard domain categories of Mathlib: the snap floor is the inverse limit in TopCat, the initial object in ModuleCat ℂ, and the initial object in the Kleisli category of the probability monad KleisliCat PMF - with no morphism returning to it in the stochastic case (the bundled witness is mc1_correspondence). What is retired is the interpretive move to call these one object: x = y across distinct categories is not a well-formed proposition, so it was never a claim to hold. (An earlier framing tried to salvage it - recasting “are the bottoms one object?” as a descent / gerbe-triviality question in the manner of Giraud, over the domains - but classical descent needs a single base site and these domains share no canonical common index, so it was a proposed frame, never an instance of a theorem; retiring the identity as ill-typed supersedes it.) What survives is the family: membership proved per domain, the members provably distinct (the walls), and the shared diagonal-fixed-point shape in the apophatic register - never a formal cross-category identity.

This framework is stated over ZF + AFA (Zermelo-Fraenkel with Anti-Foundation Axiom), not standard ZFC, and AFA permits self-containing sets (x = {x}). This affects only one commitment, the Quine atom (CC-2); the remaining results do not depend on non-well-founded sets. The Axiom of Choice is not assumed. The commitment is not the adoption of AFA specifically — a judgment about which axiom system to pick — but a set of requirements on the host theory that AFA satisfies (Tier 4); AFA is the canonical example, not the commitment itself. What “forced” means here, and the discipline every such claim must meet, is defined in Forced Metatheoretic Commitment.

The framework’s set-theoretic commitment — the property it assumes of its host theory, not the full Anti-Foundation Axiom (AFA’s “every graph has a unique decoration”) — is only the fragment that supplies a unique self-containing bottom ⊥ = {⊥}. Naming that fragment as requirements, rather than committing to “AFA specifically,” is made a checkable object in QuineHost (ZeroParadox/Settheory/QuineHost.lean): the host must supply (Y) a Quine atom ⊥ = {⊥} and (Z) its uniqueness. The third property, (X) Foundation-freeness, is not assumed — it is forced by (Y) (quineHost_not_wellFounded, axiom-free: a Quine atom is a self-loop, and no well-founded relation admits one). The rival theories then sort out — two as machine-checked theorems, Boffa by a mechanism-witness: ZFC + Foundation fails (Y) in-kernel about Mathlib’s real ZFSet (zfSet_no_quine_bottom, choice-free, via no_quine_atom — no set is self-membered under Foundation); Boffa’s axiom admits a proper class of Quine atoms rather than one (Boffa 1968; Aczel 1988), so it fails (Z) — witnessed concretely by a toy model showing self-membership alone does not force uniqueness (boffa_fails_unique), not an in-kernel result about Boffa’s axiom itself; and AFA meets all three, exhibited off the framework’s own AFAStructure (afaStructure_isQuineHost). What remains a modeling commitment — no longer “AFA is forced,” but only that (Y) and (Z) are the right requirements to demand — is a design principle; AFA is the witness that a theory meeting it exists, not the commitment. (Where AFA-specific content is used elsewhere — e.g. decoration uniqueness, APG.lean — it is proved on its own terms, not assumed from full AFA.) (The older “why AFA specifically” argument is ZP-E Remark R-AFA; this requirements framing supersedes it. It remains an argument, not a derivation in the formal system — see Tier 4 and its named falsifier.)

All proofs are machine-checked. The classical axioms that appear (Classical.choice) come from Mathlib’s computability, analysis, and ordinal libraries — they are infrastructure dependencies, not Zero Paradox commitments, and Classical.choice in Lean is distinct from the set-theoretic Axiom of Choice.

ZP-H, ZP-I, ZP-J (extension files), ZP-K, ZP-L, and ZP-M use Classical.choice via Mathlib computability, analysis, and ordinal infrastructure (Kleene’s theorem, Roger’s fixed-point theorem, metric space completion, ordinal arithmetic, and p-adic valuation). Classical.choice is the Lean kernel axiom that grounds classical excluded middle; it does not introduce non-constructive selection over infinite families of sets. The #print axioms check reports [propext, Classical.choice, Quot.sound] across ZP-I, ZP-K, ZP-L, ZP-M, and the ZP-J extension files (Scale, Model, APG); the classical axioms enter through Code/Partrec, analysis machinery, ordinal fixed-point theory, and p-adic library infrastructure, not through the ZPSemilattice or AFAStructure fields. The ZP-J core file (SetTheoryAFA.lean) and AczelConn, SelfApp, OntBridge, and WheelFrac are Classical.choice-free. ZP-P is mixed: the fork core (FixedPointFork.lean — fork_collapse_iff, fix_isEmpty) is choice-free [propext, Quot.sound], while the Ostrowski number-system instance (Ostrowski.lean — real_not_equiv_padic, completions_exhaustive) and the greatest-fixed-point side of the coalgebra instance (Coalgebra.lean — cofix_nonempty) carry Classical.choice. ZP-A through ZP-G are Classical.choice-free except where standard Mathlib theorems require it. The keystone probe files are mixed: Lawvere’s fixedPoint_of_witness / no_witness_of_fixedPointFree and Boundary’s floor_not_wellFounded are fully axiom-free (#print axioms reports no dependencies at all); the remaining results (the Lawvere face negatives, computability_face_fixedPoint, the ordinal-ascent and carrier theorems, and snap_boundary_two_registers) carry Classical.choice via Mathlib’s ordinal, recursion-theorem, and QPF machinery.