One wave function, one world.

Quantum physics lets a system be in many possible states at once, yet every measurement shows just one — textbooks patch this with a “collapse” rule added by hand. QIQT-H drops the patch. The wave function (call it Φ) is the whole of reality and never collapses; a single extra fact — λ, which just marks which of the many settled records is the one we actually experience — does the job collapse was invented for. No parallel universes, no built-in dice.

Because any region of space can hold only a finite amount of information (a well-known idea from black-hole physics), the same picture also grows a version of Einstein’s gravity. What’s unusual: every mathematical step is checked by computer (in the proof assistant Lean 4), so a skeptic can re-run the entire argument themselves. It is an honest, in-progress research program — its open problems named — not a finished theory. The rigorous version follows.

Abstract

We develop QIQT-H, a single-world, holographic formulation of quantum theory whose ontology is Φ-monism: there is one substance — the universal wave function Φ, evolving exactly unitarily — of which observers are macroscopic patterns; a non-dynamical selector λ marks exactly one decoherent record actual per run. No collapse term, no branching, no fundamental probability. The theory rests on five postulates — (P1) the (Φ,λ) ontology, (P2) quantum kinematics, (P3) microcausality, (P4) finite holographic capacity: the information content of any bounded spacetime region is finite, and (P5) quantum equilibrium of the typicality measure — of which P2–P3 are the standard quantum-relativistic arena, so the irreducible new physics is P4 + P5, on the P1 ontology. We machine-verify the entire development in Lean 4 / Mathlib: over 5,000 theorems across ~515 files, zero axioms beyond Lean's standard three, every physical input an explicitly named hypothesis.

The measurement problem dissolves without collapse: decoherence supplies the record structure, λ (P1) makes exactly one history actual, and the Born rule is reduced — provably underivable from unitarity alone, by a battery of machine-checked no-go theorems — to P5 alone. The selection layer is Poincaré-covariant, with a proved obstruction (a covariant measure exists; a covariant selector cannot) and an axiom-free boost-invariant typicality measure on the continuum 1+1D free field.

Gravity emerges holographically, in the pattern of AdS/CFT but with no string theory — and it is Φ, never the actualized branch, that carries the holographic entropy that geometry responds to. Given P4, the area floor S_vN ≤ Q_R is a derived theorem, not an added postulate (the holographic area form of Q_R enters via the conditional induced-gravity bridge, a re-derivation of standard induced gravity, not from finiteness alone); capacity-bounded record corners of an explicitly constructed crossed-product core satisfy S = A/4G as a theorem for the core's own trace-defined area; the linearized graviton (two helicity-±2 polarizations, propagating at c) carries a quantized area operator whose expectation the record count computes; the entanglement first law at every probe is equivalent to the linearized Einstein equations; Newton's constant is delivered as the relation G = 1/(N Λ_s²) (its numerical value still carried), the Sakharov ¼ is a theorem, and Strominger's BTZ boundary count equals the bulk capacity exponent at the shared granularity — the two holographic bookkeepings agree.

Every derivation is conditional on named, shrinking inputs (the Clausius/area law and the Iyer–Wald/first-law identification where not yet discharged, the matching of the trace-defined area to external geometry, the numerical value of G, the continuum Type III₁ limit, interacting matter). We claim a fully machine-verified derivation chain from finite information toward quantum gravity and single-outcome quantum mechanics — every remaining gap named, checkable, and independently auditable — not a completed theory. Any skeptic can re-run the whole chain on their own laptop: bash verify/verify.sh emits a claim card. No competing foundations program ships this.

Headlines: five results that did not exist in any proof assistant.

• The von Neumann double-commutant theorem (A″ = SOT = WOT closure — a Mathlib gap, closed).
• An unbounded Stone theorem and spectral machinery beyond Mathlib — the PVM spectral theorem, bounded Borel functional calculus, and Stone-generator reconstruction.
• towerLimitVN — the GNS inductive-limit von Neumann algebra whose Tomita–Takesaki modular theory is now complete, the first in any proof assistant: the modular operator Δ, the group Δ^it, and the conjugation J with the polar decomposition S̄ = J∘Δ^½, both halves of Tomita's theorem in full (Δ^it M Δ^−it = M and the commutation theorem J M J = M′), and a genuine non-tracial KMS state (Δ ≠ 1).
• The holographic count as a theorem (S = Σ log D = A/4G, finite branch), and the operator-level type-III₁ signature of the capacity code tower — the tower limit is a factor, non-tracial, with the full modular spectrum σ((1+Δ)⁻¹) = [0,1] (the Connes S-invariant / type classification proper stays cited — no proof assistant has a type API).
• Einstein's equations from the capacity bound (conditional Jacobson chain, free field, end to end).

Every claim, with its honest scope →

The verifiable half of quantum gravity, machine-checked — and the remaining distance is named

The honest headline still binds: this is induced / entropic gravity, machine-checked — not yet quantum gravity. What has changed is that the distance is no longer "a research program" in the vague sense. Everything that can be machine-checked given the standard physics inputs is checked, at a scale no other foundations program has; and the gap to quantum gravity proper is now one conjecture, one scaling law, and one coefficient — each with its obstruction pinned in Lean-checkable terms.

The verified half (each conditional on its named inputs): the full nonlinear Einstein equation a·T = G + Λg as a conditional theorem for the free Klein–Gordon field (qiqt_gr_freefield, on the pp-wave), with the thermal/modular side fully discharged — one-particle and field-level Bisognano–Wichmann unconditional (freeField_secondQuant_BW_unconditional); the area law derived in three independent senses (its log-additive form forced by information-composition rigidity, the ∝A scaling proved with a guard isolating boundary-locality, and S = A/4G a theorem in the constructed core); G = 1/(N Λs²) derived as a relation down to its π-transcendental content; and the operator-algebra layer no other program has (the first complete Tomita–Takesaki modular theory, the double-commutant theorem, an unbounded Stone theorem, Williamson normal form).

The remaining distance, precisely. One conjecture — the flat-space record→gravity correspondence (FlatSpaceRecordGravityCorrespondence): that in the continuum limit the capacity-bounded record code equals free QFT + linearized gravity on the emergent geometry. Its entire skeleton is now machine-checked, term by term — the continuum entropy π²/(3β), the heat-kernel form, the exact conical coefficient + c/6, the Susskind–Uglum identity S_ent = (A/4)·δ(1/G) (entanglement entropy is the counterterm renormalizing 1/G), and the saturation bridge — and 2 of its 5 physical inputs are discharged as finite theorems (the Gaussian one-loop determinant; the replica n→1 continuation giving S = −∂_n log Z_n|₁ = the von Neumann entropy). And its entailment is now machine-checked (flatSpaceCorrespondence_of_constructive): the three still-cited physical inputs — carried as explicit hypotheses, never axioms — imply the correspondence, non-vacuously (the area-law step is derived from the Susskind–Uglum identity, not assumed). So the conjecture has become a conditional theorem — the same shape as the gravity chain — whose only remaining assumptions are three named inputs: one (the curved a₁ = R/6, whose algebraic form is proved) gated on Mathlib's own Riemannian heat-kernel frontier, and two physical modeling stipulations. What stays genuinely open is the unconditional statement (discharging those three inputs + the continuum assembly): the conjecture is not proved outright — but it is no longer a bare Prop, it is a conditional theorem with a short, named, mostly-external residue. One scaling law — that the count of active modes scales with area, not volume (finiteness alone gives a volume law; area is the genuine QG-core, correctly tiered). One coefficient — the (1/6−ξ) Seeley–DeWitt number that fixes the numerical value of G, gated on a Riemannian heat-kernel result no proof assistant yet has (Mathlib's own frontier). That un-verified remainder is exactly where quantum gravity lives — and it is now theorem-shaped, not vague.

Put another way: every tractable piece is now a theorem or a cleanly-labelled conditional (its hypothesis a named structure, never a Lean axiom), so the entire remaining residue is three external walls — none of them QIQT-H-specific: Mathlib's own Riemannian heat-kernel / Seeley–DeWitt theory (its curvature half now in-flight upstream in Mathlib; the analytic heat-kernel half the deep wall), a von Neumann factor / type-classification API that no proof assistant yet has (the tower's III₁ signature is already proved), and general interacting matter (a Clay-adjacent problem). The distance to quantum gravity is now, to a striking degree, other people's infrastructure and one Millennium problem — not a private QIQT-H mystery. The open problems, in full →

1. Tomita–Takesaki modular theory — the bounded Rieffel–Van Daele modular objects (J, Δ, Δ^it) on a standard subspace, the self-adjoint modular Hamiltonian K = −log Δ as a genuine unbounded operator, and Δ^it = e^−itK as a C₀ unitary group with derived Stone generator — in any proof assistant.
2. An unbounded Stone theorem + spectral machinery beyond Mathlib — the projection-valued-measure spectral theorem for bounded self-adjoint operators, bounded Borel functional calculus with multiplicativity, the unbounded functional calculus ∫f dE, and Stone-generator reconstruction — filling a documented Mathlib gap.
3. The Araki/CGP relative entropy for the free field — the one-particle Casini–Grillo–Pontello entropy with the coherent-state reduction S_Araki(ω_W(f)Ω‖ω_Ω) = S_CGP(f), Connes cocycles included.
4. The one-particle Bisognano–Wichmann theorem — the wedge modular flow equals the geometric Lorentz boost, as an unconditional Lean theorem (free field).
5. The field-level (second-quantized) Bisognano–Wichmann theorem, unconditional — the second-quantized wedge modular automorphism acts on the whole free-field Weyl algebra as the geometric Lorentz boost, σ_t(W(u)) = W(boost(2πt)·u), with no carried BW hypothesis (discharged from the one-particle result) — lifting modular-flow = boost from one particle to the full field algebra, machine-checked end to end (free field / single mass).
6. A Jacobson "Einstein equation of state" derivation — the conditional chain from an entropy bound + Klein positivity to Einstein-form field equations (G + Λg = αT), Raychaudhuri and Bianchi machinery included, instantiated on an explicit pp-wave showcase.
7. The Sakharov induced-gravity ¼ ratio — the (conical 4π)/(EH 16π) coefficient ratio behind S = A/4G as a machine-checked theorem (the value of G stays carried).
8. The graviton's complete linearized kinematics — exactly 2 physical polarizations via the explicit gauge quotient (D(D−3)/2 = 2), helicity ±2 as explicit rotation eigenvalues e^∓2iθ, masslessness, the physical-state projector (propagator numerator), and the wave equation.
9. A canonically quantized graviton — the two helicity modes as a bosonic CCR algebra on Bargmann–Fock space: [a_i, a_j^†] = δ_ij, occupation spectrum, zero-point energy, helicity charge, coherent states, and the two-point function.
10. Weinberg's equivalence-principle theorem (algebraic core) — soft-graviton longitudinal decoupling ⟺ the Ward sum rule, and (for generic momenta) all couplings equal: massless spin-2 forces universal coupling.
11. The entanglement → linearized-Einstein bridge, assembled — the FGHMVR/Jacobson template with real parts: the first law at every probe ⟺ linearized Einstein, with the separating-probe hypothesis proven by geometric area probes, the wedge/ball Clausius data forced by the derived modular flow, and the CHM diamond conformal-Killing geometry verified by real calculus.
12. An in-model "Strominger join" — microstate count = induced entanglement area / 4G — the area defined from the calibrated entanglement cut (no separate area label), the count and the geometry agreeing as two computations of one weight family, realized by the maximum-entropy record — under a single named calibration hypothesis.
13. Code equilibrium ⟹ Einstein, and the Deser self-consistency rung — a per-ray relative-entropy-equilibrium family provably satisfies the entanglement first law at every probe and hence linearized vacuum Einstein; and the graviton's own on-shell stress is conserved, making its self-coupling gauge-consistent (bootstrap order one).
14. The Takesaki dual action and the CPW dual-weight trace on a crossed-product core — the dual action (the vector-valued Weyl relation), the exact e^−s scaling of the log-clock density, and the trace laws — traciality via the exact KMS-vs-change-of-variables cancellation (a KMS state becomes a trace under the log-clock dressing) and positivity — in any proof assistant; the von Neumann closure carried as a named hypothesis.
15. A finite holographic-screen code with a non-tautological area law — local packing ⟹ regional area bound with area an independent charge (machine-checked guards against area := log dim circularity and against the bound being free), plus min-cut/RT form.
16. Machine-checked Lorentz-violation naturalness gates (CPSUV) — the certified unsuppressed-constant theorem (the sharp-cutoff one-loop speed splitting tends to the nonzero 1/(12π²)), the covariant-regulator symmetry certificate (Δc² = 0), the diamond-tip kill (Δc² = 0 ⟺ isotropic, first-order sensitivity), and the boost-average no-regulator theorem (the null channel = W/12 exactly, divergent) — Lorentz-violation naturalness bounds in a proof assistant.
17. Frame-freeness of entropy-bound constraint sets — the covariant-capacity gate: a covariantly-transported regional entropy bound has a group-invariant admissible set, adds no speed splitting, and reopens Lorentz violation only through named channels (non-invariant preparations, background-selecting saturation, a non-equivariant enforcer, a biased selector) — each an iff-level theorem, with a genuine finite instance.
18. An operator-level emergence map: the graviton as a quantized area fluctuation — the area→metric decoder inverting the quantized area map in End(Fock); the area observables' canonical pair and vacuum fluctuations (with equal-time commutativity stated honestly); the classical entanglement→Einstein bridge recovered as the coherent shadow; the Heisenberg flow derived from an explicit scaling with the operator wave equation and the causal time-separated area commutator; and the screen code's microstate count equal to the area operator's coherent expectation over 4G — under one named expectation-level join hypothesis (the finite-code CCR isometry is provably obstructed).
19. Unitary covariance of the spectral theorem and Borel functional calculus — conjugation as a continuous star-homomorphism; the Riesz–Markov scalar spectral measures transporting as pushforwards; the spectral projections and the bounded Borel calculus conjugating (f(UTU⁻¹) = U·(f∘e)(T)·U⁻¹); and the continuum modular flow Δ^it transporting under standard-subspace carrier conjugacy — machine-checked spectral-covariance infrastructure in a proof assistant.
20. The holographic count as a theorem (finite branch) — a screen code's entropy equal to the log of its τ₀-dimension equal to induced area/4G, with the counting trace proven to be the restriction of the constructed crossed-product trace (not a new postulate), the calibration a theorem for trace-defined weights, the exact dual-scaling covariance S(θ_s·) = S(·) − s, and the clock cutoffs packaged as genuine operators with Weyl covariance — no Clausius/geometry/calibration/join hypotheses carried in this branch (the continuum walls stay named).
21. The graviton–screen-code join constructed — the emergence-map identification (the last carried join hypothesis) made a theorem: a dictionary instance with code weights defined from the geometry (links = screen elements, real trace-dimensions e^A/4G, named background apportionment), giving count = area expectation for arbitrary graviton data, the old integer-code capstone with no join hypothesis, realization of the dictionary inside the constructed crossed-product core, and the count collapsing to (A/4)·N·Λ_s² under the species-derived Newton constant — one qubit of screen record costing exactly 4·log 2/(N·Λ_s²) of area.
22. The truncated field diamond as a counted record corner — the finite-level bridge closed end to end — a multi-mode truncated free field living ON the counted screen code (the occupation basis IS the microstate space): per-mode oscillators with the honest truncation defect [a, a†] = 1 − D·P_top, one generic cross-mode commutativity theorem, records proved to be occupation pointer-basis subsets, capacity as a constraint selecting admissible cutoffs, and the capstone composing field → corner → count → area → graviton on one object with no join hypothesis.
23. A record-code dynamics with a calibration-free induced-gravity cross-check — the screen code given a genuine time evolution (diagonal Hamiltonian, records stationary, ladders rotating at mode frequencies, explicit Gibbs states with the modular flow proved to be the rescaled physical flow — the KMS certificate derived, not assumed), region entropies S(ρ_β,R) = Σ s_k(βω_k), and the saturated conditional Sakharov check S_micro(R,0) = A_ind/4G_ind whose proof provably uses none of the count's own calibration — plus the flat-space record-code/gravity correspondence stated as a machine-checked conjecture (evidence bundled and proven; the continuum claim carrying no proof field, no axiom).
24. The decoupling shadow — the dictionary's weight forced, not constructed — the finite shadow of Maldacena's decoupling structure: the free-oscillator sector proved FORCED by the capacity-cutoff limit (exact CCR recovered at bounded occupations; thermal data converging to the Planck values — the development's first genuine limit theorems), the log-capacity weight proved the UNIQUE refinement-natural area valuation (κ·Σ log D_k, with the 2-adic counterexample showing the strong hypotheses are necessary), and the REGIME-SEPARATION GUARD — a theorem that saturated capacity is provably not the free-field limit, so the two forced halves cannot be merged into a fake continuum claim.
25. The type-III₁ signature of a capacity code tower — now at the operator level — the first machine-checked contact with the Type III₁ wall: the code's Gibbs tower satisfies the arithmetic Araki–Woods III₁ criterion (hypothesis-free (1, √2) instance), separated from the Powers-factor case by a proved guard, with the σ-additive infinite-mode Gibbs limit measure and its non-atomicity. And the tower limit von Neumann algebra is now proved to be a factor (center = ℂ·1, towerLimitVN_factor), non-tracial, with the full modular spectrum σ((1+Δ)⁻¹) = [0,1] exactly (spectrum_towerResolvent_eq_Icc, operator_level_III1_signature) — the operator-level type-III₁ signature. Honest boundary: the Connes S-invariant proper and the type classification stay cited (Araki–Woods 1968; Connes 1973) — no proof assistant has a factor/type API; finite-stage Gibbs inductive-limit only.
26. The von Neumann double-commutant theorem in a proof assistant — the classical gate of operator-algebra theory, machine-checked over current Mathlib (which defines von Neumann algebras by the bicommutant property but has no bicommutant theorem): A″ = the strong-operator closure for every unital ⋆-subalgebra of B(H), with the weak-operator closure identification shipped as well (WOT = SOT = A″), the generated-algebra packaging, and the two downstream payoffs — the crossed product M⋊_σℝ and the directed-union refinement-tower limit packaged as genuine von Neumann algebras (honestly scoped: no trace extension, no type classification, tower-GNS deferred).
27. A GNS inductive-limit von Neumann algebra in a proof assistant — the capacity code tower represented on ONE Hilbert space (the completion of a deliberately semidefinite Gibbs-GNS pre-space — the direct-limit gluing done by the completion, no quotient), with a unit cyclic vector implementing every corner Gibbs state as a vector state, and the directed-union limit von Neumann algebra towerLimitVN characterized by SOT-approximation from the finite stages — the first genuinely infinite-dimensional quantum object of the program (honestly scoped: its type is NOT classified; the III₁ fingerprint stays arithmetic; Ω not shown separating).
28. A strongly continuous unitary implementation of an inductive-limit modular flow — the per-corner Gibbs modular flows transported to a strongly continuous one-parameter unitary group on the tower GNS space, fixing the cyclic vector, implementing the flow at every finite stage, and preserving the limit von Neumann algebra (honestly scoped: defined by transport — no Tomita operator, no separating claim, no Stone generator).
29. The Sakharov/Dvali species form as a rigidity theorem — 1/G = N_eff·Λ² forced for any positive, species-additive, monotone, rescaling-covariant regulator family (exponent an output, counterexample-guarded), with the first derived — not cited — heat-kernel coefficient (1/√(4πt) from the Gaussian integral) and the mixed-species consistency chain (the 1/4 and S = A/4G as theorems over one shared cited datum — honestly labelled: not an independent cross-check; no numerical G).
30. A self-adjoint Stone generator of an inductive-limit modular flow, computed on an explicit commutator core — the transported flow's unbounded generator K = K† with the cyclic vector as zero-mode (KΩ = 0), acting as the commutator [diag(log w), ·] on every finite stage of a constructively dense domain, and commuting with its own flow (honestly scoped: not claimed to be a Tomita log Δ; no PVM of the unbounded K; no exp-recovery — the recovery wall open by design).
31. A cyclic and separating vector for an inductive-limit von Neumann algebra — the standard-form hypothesis pair of Tomita–Takesaki theory exhibited in a proof assistant: the tower state's GNS vector is cyclic (dense orbit) and separating (TΩ = 0 ⟹ T = 0, via bounded right multiplications in the stage commutants and pure bicommutant algebra) for the limit algebra (honestly scoped: separation is the hypothesis for Tomita theory, not the theory — no S₀, Δ, J, KMS-at-limit, or type).
32. The Tomita operator of an inductive-limit state, computed and closable — S₀ constructed on its classical orbit domain as a genuine conjugate-linear partial operator (well-defined by separation, involutive, S₀ acting as conjugate-transpose on the dense core), with the commutant-side adjoints equal to the finite σ₋ᵢ — computed, not analytically continued — the classical Tomita pairing on a dense family, and closability in the graph-limit sense (honestly scoped: the closure, Δ, J, KMS-at-limit, and type are not constructed — the σ-semilinear closure theory is the named next Mathlib gap).
33. The closed Tomita operator S̄ of an inductive-limit state, with a conjugate-linear closure theory — four abstract theorems new to Mathlib (including the sequence-closability bridge, absent even for ordinary linear maps) deliver S̄ as an object: closed, orbit-core, fixing Ω, conjugate-transpose on the dense core, and fully involutive with trivial kernel — no adjoint and no real inner product used anywhere (honestly scoped: Δ, J, polar decomposition, KMS-at-limit, and type not constructed).
34. The modular operator Δ of an inductive-limit state, computed as the modular automorphism — Tomita's F built as a conjugate-linear adjoint on the ∃-Riesz domain (no real inner product, no dual machinery, no completeness argument), and Δ := F∘S̄: ℂ-linear, symmetric, positive, closable, fixing Ω, and acting on the dense core as the finite modular automorphism ρaρ⁻¹ stage by stage — the modular operator of the physics as a theorem (honestly scoped: Δ† = Δ is von Neumann's theorem, absent from Mathlib and the named next target; no J, polar, Δ^it, KMS-at-limit, or type).
35. Δ† = Δ — the self-adjoint modular operator, and von Neumann's theorem itself — three abstract RCLike-generic files absent from Mathlib (the self-adjointness kernel, the graph orthogonal decomposition with no adjoint anywhere, and T†T densely defined + self-adjoint for closed densely defined T), plus the conjugate-homogeneity i-twist that turns the real graph orthogonality into ran(1+Δ) = ⊤ — making the tower modular operator genuinely self-adjoint, closed, positive, with the resolvent bound (honestly scoped: no Δ^0.5, J, polar, Δ^it, KMS-at-limit, or type — the resolvent bridge to the spectral tower is the named next campaign).
36. Δ^it of an inductive-limit state — the modular unitary group, as theorems — the resolvent (1+Δ)⁻¹ as a self-adjoint contraction with spectrum in [0,1] and Δ∘R = 1−R, an abstract PVM kernel-atom + eigenvector calculus (the spectral projection at zero vanishes for injective T; f(T)x = f(r)x), and the bounded Borel calculus of R under ((1−r)/r)^it delivering a strongly continuous one-parameter unitary group that fixes Ω, commutes with Δ, and carries no junk-point spectral weight (honestly scoped: NOT identified with the transported dynamics — towerGen = log Δ is the exponential-recovery wall, the named next campaign; no KMS-at-limit, Tomita theorem, J, or type).
37. The exponential-recovery wall, crossed — towerFlow = Δ^it, and Tomita's theorem (first half) for an inductive-limit state — the Gibbs density is diagonal by construction, so matrix units are simultaneous eigenvectors of the finite modular automorphism, Δ, the resolvent, and Δ^it with identical explicit scalars: the transported physical dynamics IS the spectral modular flow of the modular operator, as operators; the generator of the physics IS the generator of Δ^it; and Δ^it implements the modular automorphisms and preserves the limit von Neumann algebra (honestly scoped: finite-stage Gibbs inductive-limit; no strip-KMS, no type).
38. The modular conjugation J, and Tomita's theorem second half in full — J M J = M′ — for an inductive-limit state — towerJ, the σ-semilinear completion of jStage a = √ρ·aᴴ·√ρ⁻¹ (no ℝ-reduction), a genuine involutive anti-unitary fixing Ω (J² = 1, JΩ = Ω, ⟪Jξ,Jη⟫ = ⟪η,ξ⟫); the polar decomposition on the core S̄ = J∘Δ^½; commutation with the modular group JΔ^it = Δ^itJ; and J conjugating left into right multiplication — giving the full commutation theorem J·towerLimitVN·J = towerLimitVN′ (tomita_commutation_equality), with Ω cyclic + separating for both M and M′. The Rieffel–Van Daele "hard half" wall has fallen — the earlier Kaplansky-gap obstruction was an artifact, closed by a classical right-boundedness estimate. So the tower now carries the complete both-halves Tomita–Takesaki commutation theorem — the first in any proof assistant. Honest boundary (never crossed): no strip-analyticity KMS; no type classification (Mathlib has no trace/factor/type API); finite-stage Gibbs inductive-limit only.
39. A genuine non-tracial KMS state for an inductive-limit von Neumann algebra (Δ ≠ 1) — the tower's Tomita–Takesaki modular theory complete — the tower vacuum vector state is provably not a trace (⟪Ω, π(E_nm)π(E_mn)Ω⟫ = w_n ≠ w_m), the modular operator is non-trivial Δ ≠ 1 and Δ^it = towerFlow ≠ id when the Gibbs weights differ — the Powers "not-the-tracial-case" separation. Together with the KMS-boundary and the full modular data (S̄, Δ, Δ† = Δ, Δ^it = the physical flow, Tomita I, J, polar-on-core, Tomita II inclusion) this is, to our knowledge, the first complete Tomita–Takesaki modular theory in any proof assistant. Honestly scoped: state non-traciality + modular non-triviality only — NOT a type classification (Mathlib has no type API); type III / S-invariant stays cited.
40. Gromov–Hausdorff limits of graph geodesics to curved metric spaces — finite graphs (and the abstract state's Bell cut-rank profile, decoded to a graph and a metric) provably GH-converge to continuum geometries: the interval, the flat torus and circle, the Euclidean cube in every dimension, a branching CAT(0) tree (the tripod — first provably non-Euclidean limit), a positively-curved cone whose curvature is a machine-checked theorem (cone_no_isometric_embedding_into_inner — no isometric embedding into any inner-product space; also from pure hop-counting), and a smooth sphere (sphereGrid_toGHSpace_tendsto_sphere). A companion layer proves the cone is flat ⟺ θ = 2π (cone_flat_iff) — the Euclidean shadow of the Hawking–Unruh temperature — pairing it with the repo's algebraic 2π (the KMS-thermal boost) in hawking_two_pi_coincidence. And it extends to Lorentzian spacetime: the reverse triangle inequality (timelike geodesics maximize proper time) for flat Minkowski (tau_reverse_triangle), a machine-checked causal no-go (why deterministic causal lattices miss the proper time — the reason causal-set theory needs random sprinkling), a continuous proper-time limit (causal_stencil_pinch), and — to our knowledge the first machine-checked curved-spacetime reverse triangle inequality — 2D de Sitter, with de Sitter horizons (tauDS_reverse_triangle, dS_causal_horizon). Honestly scoped: dimension d, angle θ, the causal order and the per-step weights are all INSERTED through the graph/state rules (not emergent), the states are CONSTRUCTED to carry the pattern, curvature = the midpoint/embedding obstruction (not a Riemann tensor), and the Hawking κβ/temperature identifications are CITED — NOT emergent dimension/spacetime, NOT GR, NOT QG.
41. Williamson's symplectic normal form, unconditional — the symplectic diagonalization of a positive-definite matrix into its symplectic (Williamson) eigenvalues (youla_pairing) — the Gaussian-state / symplectic-spectrum tool behind mode-counting and the boundary area law, a general linear-algebra theorem absent from Mathlib and, to our knowledge, from every proof assistant.

Scope, stated once for all forty-one. Free-field / linearized / conditional-on-carried-inputs where so labelled on the formalization page; none of these is a claim that quantum gravity is solved. "First to our knowledge" means: checked against Mathlib, PhysLean, and the published formalization literature as of mid-2026; we will gladly cede priority on any item shown to be formalized earlier.

P1 · The Φ, λ ontology. Φ is the complete ontology (no external observer, no fundamental probability); λ makes exactly one decoherent record actual per run — no collapse, no branching.

P2 · Quantum kinematics. Complex Hilbert space + operator algebras. The Born squared modulus is not assumed — it is the inner-product geometry of this arena (⟨k|ψ⟩ squared), forced into trace form and selected (exponent 1 over the α-family) by no-signalling.

P3 · Microcausality. Spacelike-separated regions commute — the Lorentz input. Not the source of Born: it is a machine-checked theorem that observable microcausality does not entail selector no-signalling.

P4 · The finite-information postulate (P4-MICRO / FQ). ★ The postulate is just that a region has a finite information capacity — a finite number N_R of distinguishable microstates, a UV-finite record structure. That finiteness is the whole distinctive input (the “Quantized Information” core) — and it gives only S_vN(ρ_R) ≤ log N_R; by itself it does not fix whether log N_R scales with area or volume. That the bound takes the holographic area form (log N_R ≤ A/4ℓ_P²) is derived — but in a conditional Sakharov / induced-gravity bridge (the conical-deficit heat-kernel calculation, assuming local relativistic QFT on a smooth background with a covariant UV cutoff identified with the finite microstructure), not from finiteness alone. There the area law emerges (cone curvature = δ on the boundary, integral = area) and the 1/4 is the universal ratio between the conical replica-entropy coefficient and the induced Einstein–Hilbert coefficient — two quantities sharing one UV coefficient; the ratio is machine-checked (sakharov_ratio), the value of G is not. This is a machine-checked re-derivation of the standard induced-gravity 1/4 — verified, but not unique to finiteness (any local relativistic QFT with the same UV coefficient yields it). Carried inputs: the value of ℓ_P² = G (species/cutoff), and — for the full effective action — Λ and higher-curvature terms. (2026: G can be promoted from carried to derived — positing a fundamental record-granularity scale Λ_s in place of ℓ_P gives the relation G = 1/(N Λ_s²), machine-checked axiom-free (InducedNewtonConstant), collapsing the carried inputs to a single scale Λ_s; the numerical value still needs the species accounting. And with this induced G the granularity capacity maps onto the holographic dictionary: the boundary Cardy microstate count of a BTZ horizon equals QIQT-H's bulk capacity exponent (A/4) N Λ_s² (machine-checked, HolographicBridge) — a correspondence under the shared G, not an import of a boundary CFT or AdS/CFT's cross-check.) From the finite capacity the area floor S_vN(ρ_R) ≤ A/4ℓ_P² is a derived theorem (area_floor_vonNeumann — max-entropy S_vN ≤ log dim), and for the free field the Einstein equations follow (gr_from_p4micro). It is kinematic: it does not select outcomes (that is λ's job), and there is no “capacity forbids superpositions” (H2 / Macroscopic Definiteness) postulate — that is retired as a category error.

P5 · Quantum equilibrium of λ's measure. The typicality measure is refinement-equivariant (Dürr–Goldstein–Zanghì / Valentini). This single primitive supplies the equilibrium measure from which the operational Born rule follows — both the additivity bridge and the μ-selection reduce to it. Born is not derived from nothing: it is isolated to P5, and deriving P5 remains open.

What this makes QIQT-H: a boundary theory, with “realisations” (2026). Because the only distinctive postulate on the gravity axis is finite capacity (the area form and floor being derived — the floor outright, the form conditionally), and the framework everywhere accepts a field algebra and bounds its records rather than constructing them, QIQT-H is best read not as a generative theory but as a descriptive constraint (boundary) theory on a small core (P1 + P5 + finite capacity). A generative theory — a constructive interacting QFT, the full Standard Model, a specific quantum-spacetime construction — is a realisation of QIQT-H when its regional data, encoded into the finite-capacity microstate space, satisfies the machine-checked boundary conditions: Born-weighted records, the area floor S_vN ≤ A/4ℓ_P², corner-faithful algebra (landing in the corner P·End(𝓗_R)·P, never the ambient identity), necessary bosonic truncation, no exact finite Borchers/boost scaling, the Ryu–Takayanagi area bounds (min-cut is the area, not a metric), and the selector no-go's. To realise the gravity sector it must additionally supply what the area-form derivation assumed: a smooth-background QFT, a covariant UV cutoff identified with the microstructure, the value of G, and the reference-state identification (horizon equilibrium = Bisognano–Wichmann modular and capacity-saturating).

Why this is a strength, not a hedge. The boundary is non-vacuous — it excludes theories (exact finite bosonic CCR; an anti-Born or volume-saturating selector; a region whose entropy exceeds its area). It is the same relationship thermodynamics bears to statistical mechanics, or the bootstrap to specific QFTs: the constraint layer is genuine physics precisely because it bounds. The bounds hold conditional on the postulate core being true of nature — the part experiment judges — and the open generative problems (interacting QFT, the 3+1 manifold) stay cited frontiers. In short: QIQT-H says what must hold of any region's records; a realisation is what makes it hold.

(i) Ontological, not empirical. λ is inert — no back-reaction, unobservable — so QIQT-H is operationally identical to Everett and makes no new prediction. (ii) Positing a selector is not new. It is the modal family's move (Kochen–Dieks, Bub) and structurally Bohm's (the configuration as the actuality); the idea of an actuality tag is not ours. (iii) What is ours is the verified selection schema. Machine-checked kinematics, including what fixes the record framework — einselection, via the metaselector no-go trilogy (neither capacity, nor symmetry, nor the state Φ selects it) — while λ's actual value (the seed) and the typicality measure μ remain the two open primitives.

New — the Lean-verified code–capacity bridge (2026). A small axiom-free module (CodeCapacityBridge.lean) connects the free-field substrate to the finite-microstate layer without conflating them: it keeps the field's code space C separate from the microstate space 𝓗_R and links them only by an explicit isometric encoding V : C ↪ 𝓗_R. The encoding preserves every record expectation, and — assuming the holographic-capacity postulate log dim 𝓗_R ≤ A/4ℓ_P² — it transports that bound to the field: a code that fits gives S_vN(ρ) ≤ log dim C ≤ A/4ℓ_P² and a record-count bound log(#records) ≤ A/4ℓ_P², instantiated for the actual CAR (2ⁿ) and truncated-bosonic (C(d+N, N)) field dimensions. The same formalization enforces the one structural caveat with teeth: exact finite-dimensional bosonic CCR modes are impossible (Tr[a, a†] = 0 ≠ dim 𝓗), so the photon needs a number/energy cutoff to fit a finite sector, whereas a fermionic CAR sector ⋀h is finite and fits exactly.

What this is — and is not. A capacity constraint, machine-checked: it transports an assumed finite microstate capacity through an isometric code encoding. It does not derive the holographic bound, the value of G, the Type-II renormalized entropy, or matter from information. Capacity constrains the field's entropy and records through the fitting inequality; it does not generate the field.

New — the corner construction: the field's records inside the microstate memory (2026). A follow-on axiom-free module (CornerConstruction.lean) deepens the bridge into a faithful representation of the field's records inside the microstate space. The honest device is the corner: everything carried by the encoding A ↦ VAV† lands in P·End(𝓗_R)·P with the code projector P = VV† as its unit — never the ambient identity 1_𝓗 unless the code fills the whole space. Within that discipline, all machine-checked (standard three axioms), the field's records are: faithfully read back (encoded n-point correlators equal the bare ones); Born-weighted with area-bounded information (the Born record law's Shannon entropy ≤ A/4ℓ_P²); algebraically represented — the electron's CAR transports to the corner, {ι(a), ι(a†)} = ⟨f,g⟩·P, with a guard proving that ambient-identity CAR would force P = 1, while the photon carries an explicit, surviving truncation defect [ι(a), ι(a)†] = P − N·ι(|N−1⟩⟨N−1|) (the boson is necessarily truncated in finite capacity — error quantified, not hidden); modularly structured (a finite KMS relation on the code, its modular flow living in the corner); and dynamically faithful (a supplied field flow is preserved through the encoding, with two-time correlators intact). Finally the equiprobable typicality measure (P5) is isolated: a permutation-invariant outcome law is forced uniform.

What this is — and is not. Statements about the field's records and states, not a construction of the field or its dynamics from microstates. Capacity stays a constraint, not a generator — it never derives the electron or photon — and removes neither P5 nor the capacity postulate. The continuum real-time modular flow (ρ^it, Type III) and the Gaussian/Williamson entropy–area derivation are the cited research-grade frontiers.

New — free Standard-Model field content & finite proto-spacetime, same corner (2026). Two further axiom-free modules extend the corner along the two questions everyone asks — other quantum fields and emergent spacetime — holding the same line: QIQT-H sits on top of quantum field theory (it accepts a field algebra and bounds its records), it does not construct the field, and capacity is a constraint, not a generator. (i) Fields (FreeFieldCorner.lean): one graded bracket [x,y]_ε = xy + ε·yx (ε=+1 fermionic, ε=−1 bosonic) transports into the corner, [ι(x),ι(y)]_ε = ι([x,y]_ε), and is instantiated for the whole free SM content — quarks/leptons (multi-flavor CAR → c·P), the W/Z/gluon vector bosons and the Higgs scalar (truncated bosons, each carrying the explicit surviving defect P − N·ι(|N−1⟩⟨N−1|)) — with the mode counts area-bounded; the capstone shows any free SM sector is algebra-faithful and area-bounded (S_vN ≤ A/4ℓ_P²) in the corner. (ii) Spacetime (EmergentSpacetime.lean): a no-go guard that a finite unitary conjugation can't rescale a nonzero operator (so no exact finite Borchers/boost — emergence must be approximate); the machine-checked correction that min-cut entanglement area is not a metric (it violates the triangle inequality) plus a provably-metric replacement; a finite Ryu–Takayanagi entropy skeleton with purity S(A)=S(Aᶜ) and subadditivity; the conditional finite RT inequality S_vN ≤ cut(S); and an operational causal preorder (reachability → causal cones → poset) from a supplied signalling relation.

What this is — and is not. The field side is free-field content only — interactions, non-abelian gauge dynamics, the Yang–Mills mass gap, confinement, chirality, and spontaneous symmetry breaking are cited frontiers (open mathematics). The spacetime side is finite proto-geometry with explicit error bounds — a background-independent 3+1 Lorentzian manifold and the continuum Borchers route are cited (open-physics) frontiers. The Jacobson/BW/Sakharov material below assumes a smooth spacetime, so it is emergent gravity (dynamics), not emergent spacetime (the manifold) — a distinction kept sharp throughout.

New — the quantized free graviton and the linearized bridge (2026-07). Two further axiom-free developments push the substrate to gravity's own quantum and assemble the entanglement → linearized-Einstein template from machine-checked parts. (i) The graviton (EmergentDynamics.lean, GravitonQuantization.lean): the physical polarization space is exactly 2-dimensional (the explicit gauge quotient, D(D−3)/2 = 2); the circular polarizations e_± = e₊ ± i·e_× carry helicity ±2 as explicit eigenvalues e^∓2iθ; masslessness k² = 0; the physical-state projector (the propagator numerator — idempotent, kills gauge and trace); the classical wave equation for null profiles; and canonical quantization of the two helicity modes on the Bargmann–Fock space — the CCR [a_i, a_j^†] = δ_ij, bosonic occupation, the Hamiltonian ω(N₀+N₁+1) with its zero-point energy, coherent states a|α⟩ = α|α⟩, and the two-point function ⟨0|a_ia_j^†|0⟩ = δ_ij. (ii) The bridge (BRIDGE_PLAN.md, nine increments, all landed): the quantized graviton provably solves linearized vacuum Einstein — with the converse δG = 0 ⟺ k² = 0 (Einstein forces light-cone propagation) and the linearized Bianchi identity; gauge invariance of the matter coupling ⟺ stress-energy conservation; Weinberg's equivalence principle (soft-graviton decoupling ⟹ the Ward sum rule ⟹ all couplings equal, for generic momenta); the wedge and per-ball Clausius data δ⟨K⟩ = −δS forced by the derived modular flow (given the carried BW/CHM identifications, with the CHM kernel's unit edge slope proving the wedge↔ball 2π-consistency); geometric area probes that provably separate perturbations; and the assembled capstone (bridge_conditional): entanglement first law + area law ⟹ linearized Einstein, end to end from real parts.

What this is — and is not. The graviton development is standard free-field QFT (linearized, flat background, no interactions), machine-checked — not quantum gravity. The bridge is a conditional linearized assembly: every derived step is a theorem, and every physical input is an explicit hypothesis — the Clausius/area law δS = δA/4G (the one irreducible input), the Iyer–Wald identity, the Bisognano–Wichmann/CHM identifications, scattering genericity, and the value of G. Background independence, the nonlinear completion, and the area law from microstate counting remain the cited open frontier — the quantum-gravity problem itself.

Honest scope — still a conditional formalization, not “GR from nothing.” The result remains conditional on a clearly-labelled physics floor, kept as explicit hypotheses, never as axioms: the matter equation of motion, Raychaudhuri focusing, and the per-horizon localization map — which free-field wedge mode realizes each null horizon generator, and — the genuine residual — the joint reference-state identification: that the horizon equilibrium is both the Bisognano–Wichmann modular state (which supplies the Unruh flux, β = 2π/κ) and, in its record/edge sector, capacity-saturating (S = log dim = η·A for the same area). These are different states in general (β = 2π/κ vs the maximally-mixed β = 0), so this identification is where the physical content sits. Note the entropy-area variation δS = η·δA is itself a derived theorem (differential_area_law: from the capacity bound + point-saturation + the entanglement first law — no hypothesis asserts S=ηA or δS=ηδA), so there is no separate “Clausius / area-saturation postulate” — saturation is discharged; only the joint reference identification (and the BW flux) remains. What changed this round: the modular / wedge-KMS input that earlier versions had to cite from algebraic QFT is now formalized for the free field, so the labelled surface is reduced to exactly that genuine physics — every modular, Bisognano–Wichmann, boost-charge, stress-flux, conservation, and curvature step beneath it is machine-checked (the three standard Lean axioms only). It is a verified formalization milestone — not a new physical prediction, and not a derivation of gravity from first principles. See the theorem index →  ·  Read the methods paper that produced this →

Dorau & Much, Phys. Rev. Lett. 136, 091602 (2026) — “From Quantum Relative Entropy to the Semiclassical Einstein Equations.” Public on arXiv in October 2025 and published in PRL in 2026 — before QIQT-H's gravity chain was formalized (mid-2026) — they derive, from standard algebraic QFT plus the equivalence principle, the semiclassical Einstein equations from the Araki–Uhlmann relative entropy of coherent states on a local Rindler horizon — a quantum-field-theoretic extension of Jacobson. Their chain is, step for step, the free-field gravity chain machine-checked here: modular flow = geometric boost (Fock.OneParticleBW), relative entropy = horizon energy flux (ModularEnergyBound, the first law), area variation via Raychaudhuri focusing (DifferentialAreaLaw), and Einstein's equations by stress-energy conservation (the claim card).

The honest relation — read this before you overread it. Both derivations need the same load-bearing input: the entropy–area relation S = δA/4 (Bekenstein–Hawking). They bare-assume it. QIQT-H reaches it differently — its postulate (P4) is finiteness only (strictly weaker than the area law); from it the area floor is a derived theorem, while the ∝A form and the 1/4 come conditionally from the Sakharov induced-gravity bridge (which is why there is a 1/4 left to re-derive — as QIQT-H does). So their peer-reviewed Letter — which came first — establishes the shared derivation chain — relative entropy → modular theory → Jacobson → Einstein — not the finiteness postulate itself. QIQT-H claims no priority here; what it adds is that the whole chain is kernel-checked, with every physical assumption in an explicit ledger, and that it re-derives the coefficient they take for granted. Both meet the same frontier: their closing caveat — higher-order corrections on a curved horizon, “technically demanding, especially regarding the modular data” — is precisely our cited curved-correction / Seeley–DeWitt gap.

The takeaway: a top-journal paper reached this gravity result first, as “arguments indicating.” QIQT-H independently formalized the same chain — and is the version a computer checks, the same physics reduced to a re-runnable proof.