Over the past several years I have been building a substantial formal research program — machine-verified, mathematically precise, and published with permanent DOIs on Zenodo. Today I am making the full index available at novaspivack.com/research. This post is an introduction to what the program covers and why I think it matters.

The Central Question

What must any consistent, self-contained reality look like? If a universe has no “outside” — no external model-selector, no transcendent lawgiver, no escape from the closure of its own laws — what can we prove about its structure, purely from that fact?

This is not a philosophical question in the hand-waving sense. It turns out to be a mathematical question — one that can be approached with the same rigor as a theorem in logic, and machine-checked in a proof assistant. That is exactly what the NEMS program does.

The NEMS Program: No External Model Selection

NEMS — No External Model Selection — is the core of the research program. It consists of 93 papers (plus companions), all machine-verified in Lean 4 with a strict zero-sorry, zero-custom-axiom policy. The central principle is simple: a universe with no outside cannot have its laws, parameters, or ontological ground selected by anything external. Everything must come from within.

What follows from this single commitment is remarkable. Among the results the program proves:

• The structure of gauge theory is forced. The axioms of Perfect Self-Containment (PSC) narrow the space of admissible 4D quantum field theories to SU(3)×SU(2)×U(1) with anomaly-minimal chiral matter and exactly three generations — not as an empirical coincidence, but as a theorem.
• The Born rule is the unique consistent probability assignment. In any perfectly self-contained theory with records carrying quantum effect structure, there is exactly one normalized, POVM-additive probability assignment compatible with closure: the Born rule. The uniqueness is fully machine-checked — no other assignment is consistent with PSC. Paper 14 closes the reverse direction: Born-internal complete semantics implies PSC, making the equivalence bidirectional.
• Determinism is forbidden. Diagonal-capable physical records forbid total-effective record determinism. A closed universe cannot be fully deterministic — not because of quantum randomness, but because of a deeper structural constraint.
• Non-algorithmic adjudication is necessary. Standard computation cannot resolve the indeterminacies forced by closure. Something beyond computation — what the program calls Transputation — is structurally required.
• The Simulation Hypothesis and Block Universe are refuted. The universe must be actively run from within — no total-effective static algorithm can perfectly emulate its internal adjudication. If such an emulation existed, it would produce a computable decider for record-truth, directly violating the diagonal barrier. Consequently, internal adjudicators — agents — are not biological accidents but the necessary execution engine of physical reality. The universe is not a simulation; it is a process that cannot be replaced by any description of itself.
• Physical incompleteness from universal computation. Any perfectly self-contained physical theory that contains universal computation is physically incomplete — a machine-checked diagonal barrier showing that closure and computational universality together force undecidable physical facts.
• The arrow of time follows from closure. Stable physical records and the no-overwrite constraint force the irreversibility of time as a theorem, not an assumption.
• Syntax cannot exhaust semantics. In any reflexive system, the syntactic layer cannot fully capture its own semantic content. There is always an irreducible semantic remainder — a formal no-reduction theorem for reflexive systems that closes the gap between Gödel-style incompleteness and the deeper question of meaning.
• Closure without exhaustion. Reflexive systems close without collapsing: the closure of a self-referential system does not exhaust its semantic structure. Internal semantic non-exhaustion is a theorem, not a conjecture — and it means that no reflexive system can fully describe itself, even in principle.
• Representational incompleteness. No parametric self-model can cover its own diagonal. For any attempted complete internal self-representation, there is always a blind spot — a result that closes six distinct “no-escape” routes (regress, collapse, cross-object readout, partial models, decidable self-reference, model substitution) as theorems.
• The ontological ground of reality is necessary and non-null. Paper 63 proves that if nontrivial reflexive reality exists, there must be a necessary pre-categorial ontological ground (Alpha) — not contingent, not derivable from syntax, not nihilistically empty. Paper 55 proves that qualia are irreducible semantic ledger content: the “hard problem” of consciousness, as traditionally posed, is a category error — it demands syntax alone generate qualia from outside the ledger, which is structurally impossible. Paper 70 (the Golden Bridge) unifies ground, articulation, and manifestation-in-awareness as coordinated irreducible aspects of one primordial ontological fact. The program does not merely argue these claims — it machine-checks them.

The program also covers quantum gravity, black hole information, holography, the arrow of time, institutional epistemics, self-improvement under diagonal constraints, and much more — 93 papers in all, organized into thematic groups. Every result is machine-checked. Every claim is a theorem.

Extended Mathematical Programs

Surrounding the NEMS core is a family of extended programs, each proving deep structural results about self-referential and reflexive systems:

• Infinity Compression — Proves that canonical certification cannot exhaust reflective structure. When a formal system has a bare certification layer and a richer realization layer, the two cannot be collapsed. The difference is organized by fibers, sections, and obstruction laws. The summit theorem — Reflective Non-Exhaustion — is a unified fixed-point result connecting the internal collapse barrier to the external realization gap: the enriched structure above the bare carrier is not just different, it is irreducibly richer in a precise, machine-checked sense. Seven papers, all machine-checked.
• Reflexive Architecture — A machine-checked synthesis of NEMS, Abstract Indexed Programming Systems, and Infinity Compression into a unified layered architecture. Two summits: one on closure and realization, one on what maps forget.
• Representational Incompleteness — No parametric self-model can cover its own diagonal. Six adversarial “no-escape” routes are closed as theorems.
• Reflective Fold Obstruction — If a predicate is preserved along primitive steps of an internal relation, the internal reflexive-transitive closure cannot reach any state falsifying that predicate. Fold barriers are real and structurally precise.
• Observer Non-Exhaustibility — Classifies all internal strategies for “exhausting” observer architectures into three provably blocked families, with a positive non-collapsing residual from the awareness arc of the reflexive-closure program.
• Adequacy Architecture and Reflexive Architecture Nonexhaustibility — Outer admissibility, certificate worlds, the general science of reflexive systems, and the Reflexive Development Law.

Novelty Theory

A separate program — independent of Reflexive Reality — investigates a different kind of structural constraint. Novelty Theory proves that fixed deterministic laws do not entail final explanatory closure. Even under perfectly lawful generators, there exist phase towers that no fixed admissible reducer can close. At the crown, later regimes become required for structural truths about the generator itself. This is not Gödelian incompleteness, not computational irreducibility — it is explanatory anti-closure under exact generation. A machine-checked result about why genuine novelty is not just possible but structurally necessary.

Foundational Monographs

Two book-length monographs underpin the program. The Mathematical Foundations of Self-Referential Systems develops a unified mathematical treatment from computability through transfinite and field-theoretic structure — Recursive Representation Theory, the Self-Referential Renormalization Group, information geometry, and the Self-Computation Principle. The Self-Defining Universe develops the formal theory of perfect self-containment and the meta-topological conditions under which mathematical and physical frameworks can co-emerge from closure. Both are available on Zenodo.

Why Machine Verification?

Every major result in this program is machine-checked in Lean 4, an interactive theorem prover built on dependent type theory. This means the proofs are not informal arguments — they are formal derivations that a computer has verified are logically correct, given the stated hypotheses and without any sorry placeholders or custom axioms. The Lean source code for every paper is publicly available on GitHub.

Why does this matter? Because the claims are bold. The Standard Model from first principles. The necessity of non-algorithmic processing. A formal theory of consciousness. Claims this strong invite skepticism — and they should. Machine verification is the response to that skepticism: every inference step is checked, every dependency is explicit, every assumption is declared. The work can be audited by anyone with a Lean installation.

What Is Published

All of the following are publicly available with permanent Zenodo DOIs:

• 93 NEMS physics papers (standalone PDFs, one DOI each)
• 7 Infinity Compression papers
• 17 Lean 4 software archives (the machine-checked formalizations)
• 1 NEMS corpus bundle (all 93 papers as a single archive)
• 1 PSC computational validation dataset
• 2 foundational monographs
• The Novelty Theory paper and Lean archive
• A program hub on Zenodo with hasPart / isPartOf DataCite metadata linking all 123 records

The complete index, with abstracts, DOI links, and GitHub links for every item, is at novaspivack.com/research. All Lean source repositories are public at github.com/novaspivack.

Where to Start

If you are new to the program, I recommend starting with one of these entry points depending on your background:

• General reader: Overview of the NEMS Framework (Paper 00) — the suite overview, designed to be accessible.
• Physicists: The NEMS Framework for Physicists (Paper 07) — covers gauge structure and the Standard Model derivation.
• AI / AGI researchers: Reflexive Reality: A Survey for AI and AGI Researchers (Paper 89) — theorem-grade constraints on intelligence, agency, and machine consciousness.
• Mathematicians / logicians: A Survey for Formal Theory Specialists (Paper 87) — new impossibility results and proof methods.
• Big picture: Big Results from the NEMS Program (Paper 81) — flagship theorems across all domains.
• Flagship result: Closure Without Exhaustion (Paper 91) — a theorem of internal semantic non-exhaustion for reflexive systems.

The full research index is at novaspivack.com/research. Comments, questions, and critical engagement are welcome.