Bryan Ehrlich
The claim
Quantum mechanics is the mechanics of self-modeling. A system that carries a working model of its own states and measurements, plus two imported conditions, is complex quantum mechanics with the Lüders update. The two are self-duality, the symmetry between states and effects, and a central imaginary unit in the *-envelope, for which local tomography is one co-extensive form.
Neither follows from self-modeling, and calling them operational axioms would be dressing that up. Both are imports, and both are proven irreducible by explicit models: a real qubit self-models without the imaginary unit, and a Niestegge ℓ4 system and a five-dimensional Vinberg cone self-model without self-duality. So this is a labeled synthesis with no forcing step. An earlier version of the program claimed forcing and was withdrawn.
Self-duality is worth naming plainly because it is the universal selector of the reconstruction literature. Hardy's A5, bit-symmetry, symmetric purification, pure-state transitivity and Höhn complementarity are the same condition under different names, and every reconstruction imports it somewhere. Every reconstruction of quantum theory runs on an axiom set; this is the one whose observer is defined rather than assumed.
The premise. Self-modeling means the system contains a structure-preserving model of its own states and measurements. Made precise as four clauses on a finite-dimensional spectral order unit space, it is sharp enough to prove theorems about.
The price is known. The axioms are independent - of the premise and of each other - with an explicit witnessing system for every separation: no hidden redundancy, no hidden slack. The deepest input is effect-valuedness, that the product of two effects is again an effect; on rank-two spaces with a smooth, strictly convex state ball it is the Jordan property itself. A finished companion paper carries this accounting in full.
The open question. Whether the axioms can be traded for counting: complex quantum mechanics as the dominant type among self-modeling systems by honest measure, rather than by assumption. The partial results point that way - the leading counterexample family hit a certified obstruction, and the classical alternative is suppressed by its own symmetry count. This is where the program works now.
The theorem
A. Sequential Products on Euclidean Jordan Algebras: Classification in Rank at Least Three and the Complex Qubit partially Lean-verified
Pure mathematics. On a finite-dimensional simple Euclidean Jordan algebra of rank at least three, the seven standard sequential-product axioms force the Lüders product a·b = Q√ab on the real, quaternionic and exceptional types, and leave exactly a one-real-parameter family a1/2+itba1/2−it on the complex type — with Peirce-block-diagonality of the update derived rather than assumed. Note the direction: this does not select the complex type. It shows the complex type is the least rigid one. Rigidity is what the non-complex types have.
It says nothing about observers or self-modeling — that apparatus was deliberately cut — and it imports the Jordan setting rather than deriving it. It can price a selector; it cannot supply one.
What is actually machine-checked
The paper states thirty-six numbered results. Twelve are formalized in Lean 4 against Mathlib, nineteen are partial, five aren't formalized at all. That number isn't going to 36: several results are pre-registered as external citations, and two of the four algebra types have no carrier in the development yet.
The two cases that carry the classification are done. On HN(ℝ) the Lüders product is the unique sequential product. On HN(ℂ) for N ≥ 3 the twist products are exactly the ones that survive, and the parameter is uniquely determined. Both carry the seven axioms and a dimension bound and nothing else, and both close over Lean's three core axioms alone. The quaternionic case is blocked on one transfer argument. The exceptional case has no h3(𝕂) carrier in the tree at all.
sorry. An audit file enforces both on every
declaration at build time, along with a pinned module manifest and
frozen statement boundaries, so a regression fails the build
instead of passing quietly. Every result that isn't formalized
carries a compiling certificate stating the missing step in Lean
with the gap marked, rather than a prose estimate. The prose
estimates kept decaying. That format has falsified several of its
own entries so far.
Exploratory — where the program might go
These papers were written when Paper 5's forcing theorem was still believed, and ask what else self-modeling would then force. Each survives at a conditional level (“if you grant X, then Y”); none is re-anchored to Paper A; none is ready for peer review. They map where the program might go and what the gaps are.
7. The Standard Model from Self-Modeling: Gauge Structure from the Observer-Universe Interface exploratory
Conditional on h3(O) being the arena, it houses — rather than derives — the Standard Model gauge group (U(1)×SU(2)×SU(3))/Z6 (matching the Todorov-Drenska F4∩Spin(9) result) and produces genuine parity violation (the left/right labeling is conventional, and reducing the verified left-right-symmetric content to the Standard Model's chiral form takes an extra input). The complexification step is argued, not proved — the paper's central weakness.
5. Quantum Mechanics from Self-Modeling: Deriving Complex C*-Algebraic Structure from a Single Operational Premise withdrawn
Withdrawn 2026-06-23; desk-rejected without review by JMP 2026-07-11. This claimed that four structural conditions on a finite-dimensional system force it to be isomorphic to Mn(ℂ)sa with the Lüders product, and that the complex field and C*-involution were derived rather than assumed. They were not. The program's own witnesses — a real qubit, a Niestegge ℓ4 system, a Vinberg cone — refuted the forcing claim: the two selecting steps (reciprocity and local tomography) are irreducible imports, not theorems of self-modeling. A later audit found a third, larger one hiding upstream of both. The Lean development advertised as “0 sorry, 16 axioms, each citing a published theorem” in fact encoded the unproven content in those axioms, and one of them is outright false: it asserts an inhabitant of an uninhabited structure, so that tree is inconsistent. Paper A above is the rebuilt foundation, and it is a strictly weaker and purely mathematical claim. Kept up because the record should show what was claimed.
6. The Self-Modeling Basin Is Exceptional Supergravity retracted
Retracted. This paper matched the self-modeling basin h3(O) to the exceptional entry in the GST classification of N=2 Maxwell-Einstein supergravity, and read the Einstein-Hilbert term (−R/2) in that theory's Lagrangian as a derivation of gravity. The error was conflating kinematics with dynamics. The algebra does force the kinematic structure — the 4D arena, the matter content, the cubic coupling constants. It does not force the dynamics — that the metric is a field obeying Einstein's equations. Supergravity has gravity built in by definition, so matching our kinematic data to it and finding −R/2 there recovers an assumption rather than deriving anything. Later (unpublished) work asks the algebra for the dynamics directly: a matter-sourced spin-2 mode does appear, but nothing forces the metric to obey a field equation. Honest position: the algebra fixes the arena and the matter content — the kinematics — but gravity's dynamical law looks genuinely separate. An incomplete theory, not a theory of everything. The PDF stays up as the original; a revised Paper 6 will come out of the current work.
1. Experiential Measure on the Structure Space of Self-Modeling Systems exploratory
Defines a density functional ρ on self-modeling structures and conjectures a connection to phenomenal experience. Section 10 (Lean verified) proves that ρJ = det(X)(Tr(X2)−1/3) is the unique lowest-degree F4-invariant with specific boundary conditions on h3(O). The math is clean; the interpretation as an experiential measure is a philosophical claim on top of the math, not a theorem.
Supporting & earlier results
2. Exponential Suppression of Transient-Basin Contributions in Trajectory-Weighted Markov Chain Measures
Boltzmann brain negligibility via 7-lemma composition from metastability theory. Verified.
2b. Theorem A: Lemma Assembly
All 7 constituent lemmas with error terms, citations, and dependency graph.
3. Lipschitz Stability of the Experiential Density Functional
Proves the density is Lipschitz continuous under kernel perturbations. 3000-perturbation numerical validation.
4. Falsification of the Born-Fisher-Experiential Conjecture in a Qubit Toy Model negative result
Tests and falsifies an earlier conjecture I had about ρ dynamically selecting Born probabilities. The Born rule follows from Gleason's theorem on a given algebra of rank at least three, not from the experiential measure. Published here because killing your own conjectures is part of the work. This one is unaffected by the Paper 5 withdrawal: it is a negative result about my own conjecture and stands on its own.