Plain-language introduction, illustrated companions, and reading paths for all audiences.
For the formal framework index, Lean verification, and complete question register, see README.
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.
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. |
General reader: The Philosophical Question → Foreword → any Illustrated Companion → ZP-E Companion → ZP-I Companion (framework closure)
Mathematician: ZP-A → ZP-B → ZP-C → ZP-D → ZP-E → ZP-F → ZP-J → ZP-J AFA Addendum → ZP-K → ZP-I → ZP-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-G → ZP-H (self-contained after ZP-E)
For process and methods: ZP Tools and Methods
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 |
| 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. |
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.
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:
git log to see commit history and git checkout <commit-hash> to view specific versions.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* |