ZeroParadox

The Zero Paradox: A Reader’s Guide

Plain-language introduction, illustrated companions, and reading paths for all audiences.

Lean Action CI Sponsor DOI

For the formal framework index, Lean verification, and complete question register, see README.


What This Is

The Zero Paradox proves that a minimum non-bottom element in a join-semilattice is structurally forced - not assumed. The result is machine-verified in Lean 4. The supporting structure examines what happens at the bottom element ⊥ across several mathematical frameworks; each independently locates the same structural constraint. One additional hypothesis per framework is required that is not derivable from that framework’s axioms alone - these are catalogued in Axiomatic Commitments in README.md.

Each layer of the proof is internally closed before any cross-framework claim is made.

No snap-specific axioms appear anywhere in the framework. The Binary Snap - the forced transition from the bottom element ⊥ to the minimum non-bottom state - is a theorem proved in ZP-E from A4 - the standard bottom-element axiom (∀ x, ⊥ ∨ x = x) - together with the framework’s computational commitments. A4 is a standard axiom of join-semilattice theory.


What This Is Not


Entry Point

Ask questions about the framework

This repository is connected to a Copilot Space - a GitHub AI chat with the documents and Lean source indexed. It has been given project-specific context, so it can help orient you to the layer structure and terminology.

Open Copilot Space - GitHub account required.


File Description
Zero Paradox Foreword Plain-language introduction for any reader. Start here.

Reading Paths

General reader: The Philosophical QuestionForeword → any Illustrated CompanionZP-E CompanionZP-I Companion (framework closure)

Mathematician: ZP-AZP-BZP-CZP-DZP-EZP-FZP-JZP-J AFA AddendumZP-KZP-IZP-L (axiom footprint convergence, ε₀ as snap threshold, canonical snap map) → ZP-M (Kleene-ordinal-2-adic bridge, hereditary fixed-point gap closure) - see README for the full formal index and Lean verification record

Category theory extension: ZP-GZP-H (self-contained after ZP-E)

For process and methods: ZP Tools and Methods


Illustrated Companion Documents

One companion per formal document. Plain language, diagrams, real-world examples.

Note (April 2026): Some companions were written before significant revisions to the formal documents and are currently being updated. Treat them as introductions to the framework’s structure, not authoritative statements of current theorem names or statuses.

File For Document Key Diagrams
ZP-A Illustrated Companion ZP-A Hasse diagram, one-directional transitions
ZP-B Illustrated Companion ZP-B Nested clopen balls, disjoint ball separation
ZP-C Illustrated Companion ZP-C Surprisal field singularity, 1-bit Snap cost, L-RUN execution trace
ZP-D Illustrated Companion ZP-D T map: topology → orthogonality
ZP-E Illustrated Companion ZP-E Four-framework convergence, T-SNAP derivation chain
ZP-F Illustrated Companion ZP-F ℝ vs Q₂ structural comparison, pi curve density diagram
ZP-G Illustrated Companion ZP-G Category and functor concepts, initial object, informational singularity
ZP-H Illustrated Companion ZP-H Four-functor convergence, T-SNAP derivation chain, Binary Snap across the four ZP frameworks
ZP-I Illustrated Companion ZP-I 2-adic depth diagram, three closed doors + Cauchy passage, complete cycle diagram
ZP-J Illustrated Companion ZP-J + ZP-J AFA Addendum Quine atom diagram (⊥ = {⊥}), three-way equivalence table, CC-1/CC-2 as derived propositions, abstraction chain (ValuationStructure → AFAStructure), APG decoration uniqueness
ZP-K Illustrated Companion ZP-K Four-way equivalence diagram, computational Quine, execution argument Lean verification
ZP-L Illustrated Companion ZP-L Ordinal tower with ε₀ snap threshold, dual convergence diagram
ZP-M Illustrated Companion ZP-M Kleene-Ordinal-2-adic triangle, diagonalization schema

Supporting Documents

File Description
The Philosophical Question That Started This The philosophical question that motivated the framework, and what the formal results say about it.
ZP Tools and Methods How the framework was developed: Claude’s role, what formal tools were and were not used (Rocq, Lean, etc.), the PDF rendering pipeline.

Notes on Development

This framework was developed by a human researcher in collaboration with Claude (Anthropic, April 2026). Claude served as research assistant, formal scribe, and gap identifier. All mathematical content and theoretical direction originated with the researcher. See ZP Tools and Methods for a complete account.

The PDF build tooling is publicly available in the scripts/ folder. Those scripts were generated by Claude and are included for transparency about how the documents were produced.

If you find this work valuable and would like to support its continued development, you can do so via GitHub Sponsors.


Repository and Version History

This project is hosted on GitHub at timbrigham/ZeroParadox. The repository uses Git for version control, allowing you to explore the evolution of the theorems and documents over time.

To view older versions of documents as the framework progressed:

Previous document versions are also kept in the historical/ folder, making the development process visible without requiring Git access.


For the formal framework index, axiomatic commitments, question register, and Lean verification, see README.

*Zero Paradox April 2026*