Contents
The Reflexive Reality research program is a sustained formal investigation into the deepest structural constraints on any self-contained reality — what must be true of any universe that has no “outside.” The program spans two main sub-programmes — UGP Physics and NEMS — plus adjacent formal programs, all published on Zenodo with permanent DOIs and machine-checked in Lean 4 with a zero-sorry, zero-custom-axiom policy. See the sub-programme pages for full paper listings; this page is a topline overview and navigator.
UGP Physics Programme
The Universal Generative Principle (UGP) is a deterministic, parameter-free arithmetic framework that derives the Standard Model of particle physics — its gauge group SU(3)×SU(2)×U(1), particle spectrum, particle masses, mixing angles, and cosmological structure — from a single uniquely selected integer seed (1, 73, 823) via the Generative Triple Evolution (GTE) map. There are no free parameters: every structural prediction follows from the arithmetic without empirical fitting. The Residual Classification theorem, machine-proved in Lean 4 with zero sorry, makes the Standard Model’s selection unconditional across 34,560 candidate universes. The programme spans 52 papers (P00–P51) plus 4 Lean archives and 26 tutorial documents, and produces multiple falsifiable predictions testable at Belle II, LiteBIRD, and DUNE.
★ Flagship Papers
Capstone Monograph — P48
The Complete GTE Framework
Standard Model, Gravity, Quantum Mechanics, and Cosmology from ΦMDL — zero free parameters, 334 Lean modules, zero sorry.
P01 — Founding Paper
A Deterministic Number-Theoretic Framework for the Standard Model
Introduces the GTE arithmetic framework and derives the Standard Model parameter spectrum from first principles.
P47 — Cosmology
Cosmological Predictions from the GTE/ΦMDL Framework
Dark energy, CMB spectral tilt, and gravitational wave signatures from first principles; falsifiable predictions: r = 0 (LiteBIRD), δCP = 205.71° (DUNE).
NEMS — Reflexive Reality
NEMS (No External Model Selection) is a suite of 93 machine-checked papers proving that a universe with no outside imposes precise, theorem-grade constraints on everything from logic and gauge theory to consciousness and ontology. Starting from the single principle of Perfect Self-Containment (PSC), NEMS derives results ranging from gauge group structure and the Born rule to the necessity of an ontological ground (the Alpha Theorem) and a formal theory of sentience. Surrounding the core suite is a family of extended mathematical programs — Infinity Compression, Reflexive Architecture, Representational Incompleteness, and more — proving deep structural impossibility and residual results for self-referential systems. All results are machine-checked in Lean 4.
★ Key Flagship Results
▶ Start Here
Paper 00 — For: All
Overview of the NEMS Framework
The programme portal and reader’s guide — structure, results, and how to navigate the full suite.
Paper 07 — For: Physicists
The NEMS Framework for Physicists
Self-contained introduction for physics audiences — No External Model Selection as a criterion for physical law.
Paper 81 — For: All (synthesis)
Big Results from the NEMS Program
Flagship theorems across logic, physics, consciousness, and ontology — the key results collected in one place.
▶ Flagship Theorems
Paper 91 — Capstone Result
Closure Without Exhaustion
Every reflexive system has an irreducible semantic remainder; closure without exhaustion is a theorem, not a conjecture.
Paper 11 — Logic & Physics
Physical Incompleteness
No algorithm can decide the halting problem for all PSC-consistent configurations; the universe cannot fully predict itself. Two forms, both CatAL, machine-checked.
Paper 26 — Master Fixed-Point
One Theorem Behind Gödel, Turing, Kleene, Tarski & Löb
A single master fixed-point theorem and diagonal barrier from which Gödel, Kleene, Löb, and the NEMS diagonal barrier all follow as instances.
Paper 05 — Physics
Standard Model Forced by PSC
The Two-Layer PSC Theorem uniquely selects SU(3)×SU(2)×U(1) with 3 generations from hard closure constraints alone.
Paper 14 — Quantum Mechanics
Born Rule Derived
Bidirectional equivalence: Born-internal complete semantics ↔ PSC. The Born rule is the unique quantum probability assignment in any perfectly self-contained theory.
Paper 63 — Ontology
The Alpha Theorem
The necessity of an ontological ground beyond syntax and semantics — proved from the impossibility of self-grounding.
Paper 92 — Consciousness
Consciousness, Phenomenology, and Mind
The hard problem dissolved: qualia as irreducible semantic content in Reflexive Reality — machine-checked in Lean 4.
Other Programmes
- Foundational Monographs → — Five book-length monographs providing the theoretical foundations of the Reflexive Reality program, including the UGP Foundational Monograph (P08), the Mathematical Foundations of Reflexive Reality (P13), and the Complete GTE Framework capstone (P48).
- Novelty Theory → — Machine-checked proofs of why genuine novelty is not just possible but structurally necessary: final explanatory closure is impossible even under fixed deterministic laws.
- Cognitive Computing → — Formal bounds on ML architectures: theorem-grade constraints on what machine learning systems can and cannot achieve, derived from the NEMS framework.
- Explanatory Essays → — Accessible essays on the ideas behind the formal research: 49 essays across 9 series, from the nature of self-reference to the hard problem of consciousness.
Project Status
Project status
- Program: Active — formalization and archival publication are ongoing.
- Archived works (Zenodo): 221 citable records in this family.
- Reflexive Reality / NEMS family: 132 records — the 93-paper NEMS core suite (papers 00–92), 4 companion notes, 7 Infinity Compression papers, 19 Lean software archives, 2 cognitive computing papers, Novelty Theory, 2 foundational monographs, and 4 program resources.
- UGP Physics program: 89 citable records — 55 papers (P00–P51 including P13 monograph and companions, P48 capstone monograph, P49–P51), 4 Lean repo archives (ugp-lean, ugp-physics-lean, rule110-lean, srrg-lean), corpus tarball, hub, papers bundle, and 26 Tutorial Series documents.
- Public Lean codebases (GitHub): 23 repositories covering the NEMS spine, UGP Physics application layer, and adjacent formal programs.
- Lean source (project files only): 180,209 lines of
.leanoutside toolchains/Mathlib trees; 7,631 provedtheorem/lemmadeclarations.
Lean footprint last tallied 2026-06-11 on the public repositories. Figures move forward as the program grows.
Lean Repositories
Core Lean 4 formalization archives — all published on Zenodo and browsable on GitHub. Full repo list on the sub-programme pages.
| Repository | Coverage | Links |
|---|---|---|
| ugp-lean | UGP Physics primary library: 334 modules, ridge sieve, canonical orbit, Koide theorem, gauge couplings, Braid Atlas. Zero sorry, zero custom axioms. | Zenodo · GitHub |
| ugp-physics-lean | Index of all theorem-grade results and Lean proof names across the UGP Physics programme. | Zenodo · GitHub |
| nems-lean | NEMS core self-reference library: Papers 01–51 formalized. | Zenodo · GitHub |
| reflexive-closure-lean | Reflexive closure, frontier, and awareness arc: Papers 52–70 formalized. | Zenodo · GitHub |
| rule110-lean | Cook’s Rule 110 universality theorem (P30): infinite-tape semantics, ether stability, cyclic tag system. | Zenodo · GitHub |
Full listings with all 23 repositories on the UGP Physics Programme and NEMS pages.
Is This AI-Generated?
In the era of AI-assisted science it is natural to ask how much AI was involved in this research program, and how it was used. Transparency matters, so here is an honest account.
These proofs were not generated autonomously by AI. The genesis of this project originated in the 1990s, before the advent of modern AI and proof assistants such as Lean. The ideas here are original, human-generated, and human-directed, developed over many decades before AI tools existed.
Where AI was not used: AI did not originate the theoretical ideas, direct the theoretical development, or make the underlying breakthroughs.
Where AI was used: AI was used for development and data analysis, theoretical explorations, adversarially testing ideas, helping with Lean formalization and debugging, assisting in project management, and for documentation and drafting. AI assistance made a project of this scale tractable — I made earlier attempts at developing and formalizing versions of this theory using Prolog, Scheme, and other languages, but the task was too large and the tools were not designed for it.
Computational tools: Some results made use of scientific computing tools for numerics, simulations, and computational search — including SageMath, PARI/GP, Python, NumPy, SciPy, SymPy, Pandas, scikit-learn, XGBoost, PyTorch, JAX, NetworkX, iGraph, Numba, PostgreSQL, and SAT/constraint solvers. Visualization: Matplotlib, Seaborn.
All scientific results are independently verified. Every claim labeled Category-A in the published papers is formalized in Lean 4, a formal proof assistant that mechanically checks each logical step. The Lean library contains hundreds of modules with zero unverified placeholders and zero custom axioms — the proofs depend only on the standard Mathlib library, which is itself fully machine-checked. The combination of formal proofs and independent computational verification means that every result in this programme can be audited, reproduced, and falsified.