Formalization in Lean 4 / Mathlib

The modular and relative-entropy calculus underlying the regional cost functional $\chi_R$ is machine-verified for the free-field coherent-state sector. The development carries no sorry and, as reported by #print axioms, depends only on the standard classical foundations of Lean/Mathlib (propext, Classical.choice, Quot.sound). At present the corpus spans roughly ~515 files and over 5,000 theorems (over 5,700 declarations including definitions) with a verified axiom budget of 0 (every project-specific interface axiom has been discharged to a concrete proof or a typeclass instance; what remains is carried as explicit, clearly-labelled hypotheses, never as Lean axioms).

The headline result

The coherent-state Araki relative entropy equals the one-particle Casini–Grillo–Pontello entropy, as a literal machine-checked derivative theorem:

so that

The free-field modular-energy bound (the honest core of “deriving holography”)

A related, self-contained axiom-free development formalizes the modular-energy bound — the derivable content of the JLMS route to the area law. Along this modular route the $A/4G$ area term is not free-field-derivable (the free scalar has no Newton constant $G$, no geometric area operator, a scheme-dependent cutoff coefficient, and the $\delta A/4G = 2\pi\!\int\!\delta T_{kk}$ step needs the Einstein equations) — so here the $A/4G$ identification stays a gravitational input, not a theorem. (This concerns the JLMS modular route only: the Bekenstein–Hawking $\mathbf{1/4}$ ratio is derived — as a machine-checked theorem — but through the separate Sakharov / induced-gravity bridge, SakharovRatio.sakharov_ratio (the P4-MICRO story) — a re-derivation of the standard induced-gravity ratio, not unique to finiteness (any local relativistic QFT with the same UV coefficient yields it); what neither derives is the numerical value of $G$ — though that frontier has since narrowed: the induced-Newton $1/(12\pi)$ normalization’s π-content is now derived (HeatKernelDDim: the $(4\pi t)^{-d/2}$ prefactor and the $d{=}4$ assembly to $1/(12\pi)$), and the a₁ Seeley–DeWitt $2t\cdot R$ contraction machinery is machine-checked (HeatKernelA1). The flat-space analysis is now exhausted; only the curved-space $\kappa=1/6$ coefficient stays cited — it needs the covariant heat-kernel expansion Mathlib lacks — so there is still no numerical $G$.) What is machine-checked (QIQTH/ModularEnergyBound.lean) is that the entropy variation is controlled by the modular-energy variation, which under one-particle Bisognano–Wichmann $K_\sigma = 2\pi B_{\rm boost}$ is the Unruh bound $\Delta S \le 2\pi\,\Delta\langle B_{\rm boost}\rangle$:

This upgrades the modular pieces of the carried Phase5Master hypothesis from an assumption to derived results. It is formalized modular QFT — not a derivation of the holographic $A/4G$ bound; the continuum Type III$_1\!\to$II crossed-product dual-weight trace where $A/4G$ would live remains a multi-year cited frontier.

Two 2026-07 extensions push further into that frontier. Field-level Bisognano–Wichmann is now unconditional (freeField_secondQuant_BW_unconditional): the second-quantized wedge modular automorphism acts on the whole free-field Weyl algebra as the geometric boost, $\sigma_t(W(u)) = W(\mathrm{boost}(2\pi t)\,u)$ conjugated — with no carried BW hypothesis — lifting modular-flow $=$ boost from one particle to the full field algebra. And the continuum one-particle map $j_\hbar$ is now built (Lp/Fock bricks 4–10, axiom-free): the positive-frequency map $H^{1/2}\!\oplus H^{-1/2}\!\to L^2$ with a weighted-$L^2$ isometry ($\sqrt\omega$ bounded on the right domain), the canonical symplectic normalization $\sigma = 2\hbar\,\mathrm{Im}\langle\cdot,\cdot\rangle$, and boost-covariance of $\sigma$ — embedding into the pre-existing continuum Fock tower. That is genuine progress into the Type III$_1$ continuum (not its resolution: the $A/4G$ dual-weight trace stays the cited wall).

Relatedly, InducedNewtonConstant.lean (the granularity reframing) delivers G = 1/(N Λ_s²) — G promoted from carried to derived (the relation; the numerical value still needs the species accounting) — and HolographicBridge.lean machine-checks the correspondence that, with this induced G, the AdS/CFT boundary Cardy microstate count of a BTZ horizon equals QIQT-H’s bulk capacity exponent (A/4)N Λ_s² (btz_cardy_eq_qiqth_capacity; the AdS radius cancels). This is a correspondence (the two holographic bookkeepings agree under the shared G), not an import of a boundary CFT, the Cardy formula, or AdS/CFT’s cross-check — QIQT-H’s capacity stays postulated/granularity-reframed.

Emergent gravity: the Einstein equations as a machine-checked equation of state

A second, self-contained axiom-free development formalizes Jacobson’s “Einstein equation of state” route to general relativity — with the thermodynamic input now grounded in QIQT-H rather than assumed. The result is a single conditional theorem:

qiqt_gr_from_wedge_kms — the Einstein field equations $a\,T_{\mu\nu} = G_{\mu\nu} + \Lambda\,g_{\mu\nu}$ (with a genuine Einstein tensor and a constant $\Lambda$) follow from QIQT-H’s holographic capacity bound $S \le \eta A$ together with Klein positivity $S(\rho\Vert\sigma)\ge 0$, modulo exactly three clearly-labelled, well-motivated physics inputs: the wedge KMS property, matter conservation $\nabla^\mu T_{\mu\nu}=0$, and standard structural regularity.

What is genuinely derived inside the chain (no hypothesis smuggles in the conclusion):

• the differential area law $\delta S = \eta\,\delta A$ — from the capacity bound + saturation at the reference + Klein positivity (no hypothesis asserts $S=\eta A$; the inequality side is QIQT-H’s own theorem);
• the boost-charge content of input #1 — the wedge modular flow is the geometric Lorentz boost (one-particle Bisognano–Wichmann), and the boost-energy derivative is purely imaginary, $i\cdot(\text{real})$, from the explicit boost generator together with unitarity;
• the focusing content of input #3 — at a stationary horizon the Raychaudhuri equation collapses to pure Ricci focusing $\,\mathrm{d}\theta/\mathrm{d}\lambda = -R_{kk}$;
• all the differential geometry — the Bianchi identities, $\nabla^\mu G_{\mu\nu}=0$, the null-cone $\Rightarrow$ tensor step, and the constancy of $\Lambda$.

The instantiated showcase — the floor laid bare

The development since has been drained further: the chain is now machine-checked for an explicit free Klein–Gordon field on a curved pp-wave spacetime, the one-particle Bisognano–Wichmann theorem is now a fully unconditional Lean theorem (no longer a cited input), matter conservation $\nabla^\mu T_{\mu\nu}=0$ is derived for the KG stress tensor, and the entropy/area derivatives are derived from smoothness of the record law. The capstone of that effort is a single theorem that discharges every geometric and analytic premise and exhibits exactly what GR rests on:

qiqt_gr_ppwave_showcase — the Einstein field equations $a\,T_{\mu\nu}=G_{\mu\nu}+\Lambda g_{\mu\nu}$ for the explicit pp-wave spacetime, with the metric/tetrad, the area derivative (Raychaudhuri area-rate, via an expansion-free congruence), and the entropy bound $S\le\eta A$ (Shannon’s maximum at the holographic capacity) all discharged inside the theorem — leaving as hypotheses exactly the irreducible floor.

The localization map is provably not dischargeable by analysis: at the uniform reference the Shannon entropy is stationary ($\sum p'=0$), so the value of the heat rate is forced to be the stress flux — i.e. the field-coupled record law, the irreducible Gap-2 input. So the showcase is the cleanest honest statement of the result: the Einstein equations for the pp-wave spacetime follow from the matter equation of motion + the holographic capacity (P4) + the localization map — every geometric, curvature, area-kinematic, and entropy-bound step machine-checked and discharged.

The quantized graviton and the linearized bridge

Two further axiom-free developments (2026-07) extend the substrate from the scalar field to gravity’s own quantum and assemble the entanglement → linearized-Einstein bridge from machine-checked parts.

The free graviton, end to end

The linearized graviton is now formalized from kinematics through canonical quantization — standard free-field physics, machine-checked (every theorem axiom-free, standard 3):

The bridge: entanglement first law ⟺ linearized Einstein, assembled from real parts

The FGHMVR/Jacobson template (entanglement first law at every ball ⟺ linearized Einstein) is assembled in nine increments — every derived step a theorem, every physical input an explicit hypothesis (never a Lean axiom):

The microtheory earns its gravity (E1–E5)

A follow-on campaign of joins between held theorems upgrades the bridge from assembled to earned in-model (all axiom-free, standard 3):

The wall: the Type II dual-weight trace on the crossed-product core (W1–W4)

The Chandrasekaran–Penington–Witten dual-weight trace — the object whose renormalized entropy underlies the Type II capacity story — constructed on an honest algebraic core with its three defining laws exact (all axiom-free, standard 3):

Index of machine-checked results

For the exact theorem statements, machine-translated from the Lean source to readable math (notation only, content verbatim), see the machine-rendered statements page.

Toolchain leanprover/lean4:v4.30.0 · verified in QIQTH/AxiomAudit.lean.

Finite Araki relative entropy

Operator convexity → Lieb’s concavity → DPI → strong subadditivity

A complete, axiom-free, finite-dimensional formalization of the Carlen DPI–Lieb tower — operator-convexity machinery that Mathlib does not have — built bottom-up, every result standard-3. This is an independently-useful contribution to formalized mathematics, and it is what discharged the program’s former entropy-interface axioms (Donald, DPI, ArakiInterface, EntropyBridge) outright.

Bounded Tomita–Takesaki (standard subspace)

One-particle CGP relative entropy

Free-field (Fock) modular flow

Coherent-state relative modular operator and reduction

Free-field Born measure & decoherent-histories consistency

A genuine (non-deterministic) Born probability measure on the continuum free field, its Lorentz-covariance, and the decoherent-histories consistency (sum-rule) conditions. Born is the input weight $\mu_\Phi(\alpha)=\lVert C_\alpha\Phi\rVert^2$; these theorems establish that it is a consistent, $\sigma$-additive, covariant probability — not a derivation of Born.

The metaselector — what fixes the record framework

The choice of abelian record framework $\{P_\alpha\}$ resolved as a no-go trilogy (neither capacity, nor symmetry, nor the state $\Phi$ selects it) plus a positive selector (einselection), with a category-error-proof record/area “contract.” Verified scaffold, not new physics: $\lambda$ stays inert, so the scheme remains operationally Everett (an ontological reading, with no formal-content claim attached).

Born from typicality — the symmetry / state-supervenience reduction

The Born weights reduced from typicality to a single state-supervenience premise (with a no-go that some premise is unavoidable). Born is input, not derived; these establish what it reduces to.

λ’s selection schema: covariance & contextuality (OP3b)

λ’s selection schema: the finite Takesaki criterion + modular invariance

The finite (Type I) shadow of λ’s kinematic-and-dynamical law. λ is Type-III-native — the records it selects come from a chosen abelian pointer subalgebra 𝔄 (which exists already inside a Type III₁ factor), and the Born weights are the algebraic state value $\omega(P_\alpha)$, needing no trace. These theorems make precise which 𝔄 is consistent, that the decoherence map is the conditional expectation onto it, and that the selection is stable under the modular dynamics.

λ’s selection schema in the continuum (free-field / standard-subspace sector)

The finite schema above, lifted onto the genuine continuum modular flow $\Delta^{it}$ (the Rieffel–Van Daele bounded modUnitary of a standard subspace) — axiom-free. The local algebra’s Type III₁-ness (Buchholz–Wichmann) is cited; the residual walls are the Haagerup natural-cone existence in Mathlib and the interacting case.

And the whole schema lifted to the second-quantized free field: $\Gamma(\Delta^{it})$ as a unitary one-parameter group of bounded operators on the Fock Hilbert space, with the field-level automorphism, modular-invariance, Born rule (on the genuine Fock vacuum state) and selection event.

The joins — hypothesis deletion (J1–J4)

A dedicated campaign shrinking the carried inputs of the landed results by connecting held theorems. The ledger, entry by entry (each says which named hypothesis became a theorem or shrank):

• J1 — the finite corner discharges the eigen-core matter inputs (finiteCorner_tau_trace, finiteCorner_tau_pos): the constructed Type II trace’s traciality and positivity hold on the concrete corner (ρ = diag p, matrix units, κ_ij = log p_i − log p_j) with no matter hypotheses — the KMS-eigen law, frequency conservation (automatic from the matrix-unit index loop) and positivity are theorems. Deleted (for this model): hkms, hfreq, hpos.
• J2 — the CHM kernel probe + bridge refactor (chmRadialMass3_eq = 4πR⁴/15, CHMSymbolProbe3_eq, bridge_conditional_probe): the mass-normalized CHM kernel pairing equals the ray area probe (one-variable calculus), and the bridge consumes the derivable probe. The Iyer–Wald input factors; the residual is one stated identification (hDeficit).
• J3 — the abstract CHM transport theorem (hCHM_of_conformal_transport, toBallModularFamily): the per-ball CHM identification is a theorem of ONE carried massless wedge-BW datum + conformal conjugacy + the modular transport in its weakest form (the m > 0 BW theorem is never instantiated at m = 0). hCHM (per-ball physics) shrunk to a wedge datum + functoriality + geometry — and the functoriality (hmodVac) has since been DELETED by the grounding campaign below.
• J4 — the formal Deser system (next_source_conserved, extend_of_solver, einsteinDeserSystem): all-order consistency propagation — the next source’s conservation is derived from a solving tower (harmonics at their correct momenta n·k; the Bianchi identity proven at every harmonic); no tower positing conservation per order. Order 2 stays the concrete Deser theorem; nonlinear coefficients = frontier.

The Lorentz stress-test gates (CPSUV → diamond tip → state level)

Three falsification gates on the finite-capacity postulate itself — numerics validated against closed forms, the decisive constants and limits machine-checked (QIQTH/QG/CpsuvGate.lean, LatticeDispersionBound.lean, DiamondTipGate.lean, StateLevelLVGate.lean; scripts lorentz_stress_test.py, diamond_tip_test.py; results docs under docs/qg_roadmap/).

• Gate 1 — CPSUV. A preferred-frame spatial cutoff in interacting Yukawa theory generates the one-loop speed splitting Δc² → g²/12π² — an unsuppressed constant (cpsuv_gate_sharp_fails: the closed form’s nonzero limit is a Lean theorem; quadrature matched to 2·10⁻¹⁸); any O(4)-invariant regulator gives Δc² = 0 by symmetry (covariantSplit_eq_zero). The naive mode-cutoff reading of finite capacity is falsified; the free-field lattice pass (|E_a² − (m²+p²)| ≤ a²p⁴/12, also a theorem) is certified NOT decisive.
• Gate 2 — the diamond tip. A causal diamond’s tip vector u^μ_D does reach the effective action: within the anisotropic family the splitting vanishes iff the regulator is isotropic (tipSplit_eq_zero_iff), with first-order sensitivity −2C ≠ 0; and the rapidity-average escape fails provably — the boost-averaged cutoff’s null channel equals W/12 exactly (boostAvg_log_channel, boostAvg_diverges): linear growth, not a regulator. There is no local Lorentz-invariant finite-capacity cutoff; frame-averaging cannot manufacture one.
• Gate 3 — the state level. The surviving reading — Q_D bounds the entropy of the diamond algebra in the covariant vacuum — makes no low-energy LV prediction: the admissible set is frame-free (admissible_smul_iff, constraintSet_invariant), the constraint touches no propagator (stateLevel_noDeltaC2: Δc² = 0 identically), and the only reopening channels are named theorems — non-invariant prepared states (operationalLV_iff_not_invariant), background-selecting saturation (conditioned_invariant_iff_orbit_constant), a non-equivariant enforcement mechanism (equivariant_enforcement_preserves_invariance), or a biased selector (closed by the held upvm_covariant_probability). Genuine finite instance: permutationCapacity.

The operator emergence map — “graviton = quantized area fluctuation,” theorem-shaped (Q1–Q5)

The classical area→metric decoder promoted to an operator map on the polynomial Bargmann–Fock carrier (Module.End of ℂ[X₀,X₁]; the completion is never used as an operator domain). Two honesty rules are machine-enforced by design: equal-time quantized areas commute (the naive noncommutativity claim was cut at consult time), and the finite code can never carry exact CCR (the trace obstruction) — the code join is expectation-level, permanently.

• Q1 — reconstruct_hHat: the decoder inverts the QUANTIZED area map at operator level — the metric operator ĥ is a function of its own area-fluctuation observables, entrywise in End(Fock).
• Q2 — comm_area_mom, vacuum_area_pair: the honest quantum structure — the canonical pair [Â(Σ), Π̂(Σ′)] = i·areaPair·1 and the vacuum fluctuation ⟨0|Â(Σ)Â(Σ′)|0⟩ = areaPair(Σ,Σ′); equal-time areas commute (comm_area_area = 0).
• Q3 — coherent_hHat, coherent_area: the classical bridge is the coherent shadow — ⟨α|ĥ|α⟩ = h(α) = Σ_λ 2Re(α_λ)·pol^λ and ⟨α|Â(Σ)|α⟩ = δA_Σ(h(α)): exactly the δA input the assembled first-law ⟺ Einstein skeleton consumes.
• Q4 — heis_q, hHatT_wave, comm_areaT: the Heisenberg flow derived from the explicit monomial scaling (no Stone theorem), the operator wave equation ḧ + ω²ĥ = 0 (coefficientwise), and the time-separated area commutator 2i·sin(ω(s−t))·areaPair·1 — the causal structure of quantized areas.
• Q5 — code_count_eq_fock_area_expect (THE JOIN): with the held calibration and ONE named carried input hJoin (induced screen area = coherent total-area expectation, Â_tot = A₀·1 + Â), log #microstates = ⟨α|Â_tot(Σ)|α⟩ / 4G — the screen code’s counting and the graviton’s area operator agree as two computations of one number.

The grounding campaign — carried hinges deleted at once (G1–G5)

Two files, four increments; every deletion names its residue.

• G1 — the Bargmann adjointness (bargmann_adjoint, coeffFamilyPair_cohCoeff, cohPair_X_mul): creation is adjoint to annihilation on the polynomial Bargmann–Fock space (⟨p, X_l·q⟩_B = ⟨∂_lp, q⟩_B), with the coherent reproducing rule ⟨coh α, p⟩_B = p(ᾱ). The operator-emergence coherent v-rule — previously cited — is now a polynomial-level theorem; the completion-level identification stays cited.
• G2 — the RvD operator transports (rvdRC_transport): R_S′ = U R_S U⁻¹ from orthogonal-projection uniqueness under the ℝ-isometry; i𝒦 transports automatically by ℂ-linearity.
• G3 — the unitary covariance of the spectral theorem and Borel calculus (cfc_conjU, specMeasure_conjU, specProj_conjU, borelFC_conjU): the continuous calculus, the Riesz–Markov scalar measures (as pushforwards, with Tietze-extended ambient tests), the spectral projections, and the bounded Borel calculus — f(UTU⁻¹) = U·(f∘e)(T)·U⁻¹ — all transport. New spectral-tower infrastructure, independent of this campaign’s payoffs.
• G4 — the modular flow transports; three payoffs (modUnitary_transport): Δ^it conjugates under carrier conjugacy. J3’s hmodVac carried field is DELETED (the ball-transport package builds from geometric carrier conjugacy alone — residue: the geometry + the massless wedge BW); Gate 3’s covariance hinge is fed by the derived modUnitary_inner_cov; the ball-Clausius per-ball modular input is replaced by per-ball geometry.

The keystone — THE COUNT (K0–K6): the holographic count as a theorem in the finite branch

The campaign derives, rather than posits, that a diamond/screen algebra’s entropy against the constructed crossed-product trace τ₀ equals induced area/4G — deleting, in the finite branch, the Clausius input, the geometric input, the calibration log D_e = w_Ent(e), and the emergence join at once (QIQTH/Keystone.lean, KeystoneOperator.lean; axiom-free, std-3).

• K0 — the entropy substrate (vonNeumannEntropy_maxMixed, vonNeumannEntropy_le_log_card): S(maximally mixed) = log N against the UNNORMALIZED counting trace, with the Gibbs/Jensen guard S(ρ) ≤ log N for every density — the count equality is claimed only where it holds.
• K2a — the standalone finite count (K2a_count_capstone): link dimensions D_e, microstates N_C = Π D_e, the diamond matrix algebra with τ(1) = N_C, record projections with τ(P_R) = |R| (the trace COUNTS records), and S = Σ_e log D_e = A_τ(C)/4G as a theorem — G entering only through the normalization. The boundary is itself a theorem: count_matches_external_weights_iff — matching EXTERNAL geometric weights is the old calibration, never counted as deleted.
• K2b — THE COUNT IN THE HELD CORE (tauMonomial_uniform_eq_tauCount, wEntTau_eq_log_tau0Dim, K2b_tau0_capstone): the counting trace IS the restriction of the constructed crossed-product trace τ₀ — the held monomial-trace formula at the uniform matter state and a mass-N_C clock window reproduces Tr x exactly, so the count is not a new postulate; and the calibration is a theorem because the weight is trace-defined (the link weight IS the log of the link fiber’s τ₀-dimension). Capstone: S(record corner) = log dim_τ₀(𝒟_C) = A_τ(C)/4G.
• K5 — the covariance checks (tauCount_conj, K5_dual_covariant_count): trace-preserving code unitaries preserve the count; the dual action SCALES it exactly — S(θ_s·) = S(·) − s, the honest transported-area covariance law (never naive invariance).
• K1 — the operator packaging (clockMul, clockTransl_clockMul, repMonomial): bounded-symbol clock multiplication operators on L²(ℝ; H), the product law, the Weyl covariance λ_t∘M_g = M_g(·+t)∘λ_t, and the represented core monomial π(a)·λ_t·M_F as a genuine continuous operator.
• K3 — finite closure hygiene + a soundness find (tauCount_norm_le_sum_diag): the counting trace is bounded on the finite corner; and the carried vN-extension interface (DualWeightTraceExtension) was found VACUOUS — an abelian collapse witness (M = ℂ) satisfied it for any algebra — and strengthened with a multiplicative-embedding requirement that provably kills the witness. No fake finite instance was shipped; the genuine σ-weak/normal-weight extension stays a named wall, now carried non-vacuously.

The join instance — hJoin deleted by construction (JI1–JI7): the two towers merged

The screen-code tower (the keystone count) and the graviton tower (Q1–Q5) joined into ONE object at the finite level: the dictionary instance — links = screen elements, code weights defined FROM the geometry — makes the Q5 carried hypothesis hJoin a theorem (QIQTH/JoinInstance.lean; axiom-free, std-3). Two-level construction per the consult verdict: generic-exact with REAL trace-dimensions; integer codes only under a named realizability datum.

• JI1 — the local area decomposition (sum_localArea, A0Split): the per-element shares β_a + δA_a reassemble A₀ + δA_Σ(h), with the background apportionment carried as NAMED data (no canonical per-link split of a global constant exists; the uniform split is an optional policy, never pretended-derived).
• JI2 — the carried hJoin is a THEOREM (hJoin_tau, hcal_tau): with w_Ent(a) := A^loc_a/4G and D^τ_a := e^w (a positive REAL — trace-dimensions need not be integers), the exact Q5 hypothesis shape is supplied by construction, and the calibration is Real.log_exp. Geometry → code: no smuggling.
• JI3 — the dictionary lives in the held core (exists_tau0_corner_of_posReal): every positive real is a realized τ₀ corner value with the clock-window witness explicit (the free window mass — never subcorners of one fixed fiber+window, which are provably rank-quantized).
• JI4 — the generic exact replacement (Stau_eq_area_over_4G): the instance’s count S_τ(J) = Σ_a w_Ent(a) = A_J/4G for ARBITRARY graviton data — count and geometry as two computations of one number, nothing carried.
• JI5 — the old Q5 capstone with NO hJoin hypothesis (code_count_eq_fock_area_expect_noJoin): for a nat-realizable geometry (NatRealizable — the named integer-dimension datum, where D^τ_a = D_a), log #microstates = ⟨α|Â_tot(Σ)|α⟩/4G with the join supplied by hJoin_tau.
• JI6 — the two normalizations are one formula (Stau_eq_capacity_primitives): with the DERIVED G = 1/(N·Λ_s²), the count is S_τ(J) = (A_J/4)·N·Λ_s² — the count-built and induced-Newton normalizations meet in {area, species, granularity}; per-link capacity, the patch bound, and the area costs: one nat of link entropy costs 4/(N·Λ_s²) of area; one qubit costs 4·log 2/(N·Λ_s²).

The embedding — the truncated field diamond IS a counted record corner (EM1–EM7): the finite-level bridge closed

The matter-side dictionary. The key observation is definitional: the keystone’s microstate space Micro = Π_k Fin(D_k) IS a multi-mode truncated Fock basis (joint occupation numbers n_k < D_k) — no new Hilbert space is built; the campaign gives the already-counted diamond algebra its FIELD structure and the mode↔link semantics (QIQTH/Embedding.lean; axiom-free, std-3). With THE COUNT, THE JOIN INSTANCE, and THE EMBEDDING complete, the finite-level bridge is closed end to end: a truncated free field in a diamond IS a counted record corner, its records ARE occupation pointer states, its count IS the area over 4G, and that same number IS the graviton’s coherent area expectation — one object, one theorem chain.

• EM1 — the dictionary (ModeAssignment, truncated_field_diamond_entropy): a LINK IS A FIELD MODE (dimension = truncation cutoff, named finite data); the keystone count reads verbatim as the truncated field diamond’s entropy S = Σ_k log D_k = A_τ(C)/4G.
• EM2 — the coordinate embedding (modeOp + transport package): direct-entry (A on fiber k, delta elsewhere — never Kronecker), unital/additive/multiplicative/⋆/injective via a reusable fiber-sum lemma — each single-mode oscillator algebra genuinely embeds.
• EM3 — the per-mode oscillators (mode_ladder_commutator): the HONEST transported defect [a_k, a_k†] = 1 − D_k·P_top,k (exact CCR permanently impossible — stated, not hidden); the finite spectrum reading; [N_k, a_k] = −a_k.
• EM4 — the cross-mode algebra (modeOp_commute_of_ne): ONE generic theorem, all cross commutators as corollaries — the bosonic sector (fermionic CAR needs the held graded layer).
• EM5 — records (recordProj_eq_sum_occupationProj, encoded_mode_ladder_commutator): RECORDS ARE OCCUPATION POINTER-BASIS SUBSETS as a theorem (welding the record ontology to the field ontology); the record trace through the constructed τ₀; corner transport with the honest unit P = VVᴴ, never the ambient 1.
• EM6 — capacity (field_entropy_le_area_of_capacity): CAPACITY IS A CONSTRAINT, NOT A GENERATOR — Σ log D_k ≤ A/4G selects admissible assignments and implies S ≤ A/4G; each mode occupies 4G·log D_k of area; ≤ A/(4G·log 2) two-level modes per diamond.
• EM7 — the capstone (truncated_field_count_eq_fock_area_expect_noJoin): the finite-level bridge end to end — log #(truncated Fock basis) = ⟨α|Â_tot(Σ)|α⟩/(4G), composing field → corner → count → area → graviton on ONE object with no join hypothesis; LocalizedModeFrame certifies (never constructs) localization.

The dynamics — the code’s time evolution, the independent cross-check, and the conjecture (DY1–DY7)

The microscopic side gets what a definition of a theory requires — a time evolution — and the campaign closes with the QIQT-H analogue of the Brown–Henneaux = Cardy check in its honest finite form, plus the sharp continuum conjecture stated (never assumed) in Lean (QIQTH/Dynamics.lean, CrossCheck.lean, Conjectures.lean; axiom-free, std-3).

• DY1 — the diagonal dynamics (alpha, the entry formula): H = Σ_k ω_kN_k with its Heisenberg flow via explicit phase unitaries (no Stone theorem, no matrix exponential) — a one-parameter group of ⋆-automorphisms under which records are stationary (the honesty point: H is a function of the N_k, so what λ selects among does not move) while the ladders rotate, α_t(a_k) = e^{−iω_k t}a_k.
• DY2 — the explicit thermal state (gibbsDensity): a product diagonal density (per-mode Boltzmann weights), a genuine density for every β, stationary under the flow.
• DY3 — the KMS bridge (sigmaDiag_gibbs_eq_alpha_rescale): the Gibbs state’s modular flow IS the rescaled physical flow, σ_s^ρ_β = α_−βs (the partition function cancels; the flow is never defined by modular theory — the bridge runs from the independent dynamics to the KMS certificate); at β = 0 the Gibbs state IS the keystone’s maximally mixed counting state.
• DY4–DY5 — regions and their entropy (marginal_gibbsWeight, entropy_gibbs_region): regions = subsets of mode labels (no spatial-entanglement claims); the Gibbs marginal is again Gibbs; S(ρ_β,R) = Σ_k∈R s_k(βω_k), saturating at Σ log D_k with the all-β Gibbs bound.
• DY6 — the saturated conditional Sakharov cross-check, CALIBRATION-FREE (S_micro_zero_eq_inducedQuarterG): the code dynamics’ region entropy at saturation equals the induced area over 4G_ind — the microscopic side computed from the Hamiltonian, the macroscopic side supplied by independent Sakharov/species/cell data (with the derived G_ind = 1/(N_eff·Λ_s²) only the species/cell matching remains input), and the proofs referencing NONE of the keystone calibration (grep-verified). Equality at saturation ONLY; the arbitrary-β equality is false and never claimed.
• DY7 — the conjecture (FlatSpaceRecordGravityCorrespondence): the flat-space record-code/gravity correspondence, stated sharp — in the continuum limit the capacity-bounded record code with diagonal dynamics equals free QFT + linearized gravity: for every region, micro record entropy = one-loop conical entropy = area/4G_ind, with G_ind the Sakharov constant of the SAME field content (one microscopic system computing both the states and G). The DY1–DY6 evidence is bundled and PROVEN (finiteEvidence_holds); the continuum claim carries NO proof field, NO axiom, NO instance — stated, never assumed.

The decoupling shadow — the finite forced core of the dictionary (DS1–DS7)

Prompted by a primary-source re-reading of Maldacena (hep-th/9711200), whose deepest structural feature is that the dual sides are two SURVIVING DESCRIPTIONS of one parent construction under one limit: this campaign delivers the honest finite shadow of that structure — the word “constructed” is deleted from every part of QIQT-H’s dictionary where deleting it is mathematically true, and what remains is named parent data (QIQTH/Decoupling/, QIQTH/Rigidity/; axiom-free, std-3).

• DS1 — the free sector forced, operator level (commutator_eventually_exact): at fixed occupations the truncated ladder matrix elements are D-independent and the commutator entries stabilize to the exact-CCR values — the truncation defect lives only at the top level, which bounded occupations eventually never see.
• DS2 — the first genuine limit theorems (tendsto_meanN, tendsto_defectExpect): at fixed βω > 0 the truncated occupation converges to the PLANCK value q/(1−q) and the defect expectation dies — the state-level decoupling half, bridged to the code’s own thermal states.
• DS3 — THE REGIME-SEPARATION GUARD (guard_entropy_saturates, guard_defect_survives): along ANY schedule x_D·D → 0, capacity saturates BUT the defect expectation tends to 1, not 0 — exact saturated capacity is provably NOT the positive-temperature free-oscillator limit. The two halves of the shadow live in different regimes, as a theorem: the formalization itself forbids merging the count and the field limit into a fake continuum claim.
• DS4 — the finite-product lifts (tendsto_productEntropy): entropies, defects, and fixed occupations’ Gibbs weights of finite mode sets all converge to the free-field values.
• DS5 — the Cauchy rigidity (monotone_logValuation): monotone additive on ℝ is linear (proved by hand); a monotone product-to-sum valuation on ℝ>0 is κ·log.
• DS6 — THE FORCED WEIGHT (finiteCorner_valuation_rigidity, forced_weight_product, nu2_counterexample): a monoidal valuation monotone under ALL isometric embeddings is forced to be κ·log n — hence on product record corners A = κ·Σ log D_k: the local weight of the keystone/join/embedding dictionaries is the UNIQUE refinement-natural valuation, no longer a constructed choice (κ is the one free normalization — where 4G lives, input). Necessity is machine-checked: ν₂ is additive and divisibility-monotone yet not ∝ log — the strong hypotheses cannot be weakened.
• DS7 — the shadow package (decouplingShadow_holds, saturated_entropy_eq_forced_area): the parent tower with its three theorems — the free sector survives the cutoff limit; every refinement-natural valuation is κ·Σ log D_k; given the normalization, the saturated area law survives (the code’s β = 0 entropy = the forced area over κ).

The tower (T1–T8): the first machine-checked contact with the Type III₁ wall

Phase A of the continuum-definition attack, via the ITPFI/Araki–Woods route: the capacity code tower with its Gibbs product states IS Araki–Woods input data, and its arithmetic invariant is machine-verified to be the III₁ one — at the level of the wall’s fingerprint, never the wall itself (QIQTH/Tower/; axiom-free, std-3).

• T1 — the fingerprint predicates (IsTailModularExponent, AWFingerprintIII1): the named witness form of the Araki–Woods asymptotic-ratio invariant, additive in the modular exponent κ, with a load-bearing tail quantifier and uniform weight floor (drifting-frequency and vanishing-weight counterexamples documented), the EXACT per-mode ratio λ₁/λ₀ = e^{−x} (the partition function cancels), and the bridges to the held kappaOf eigenvalue law.
• T2 — Kronecker density: two reals at irrational ratio generate a dense additive subgroup (AddSubgroup.dense_or_cyclic; the cyclic case forces a rational ratio).
• T3 — THE CENTERPIECE (gibbsTower_awFingerprint_III₁): two frequencies occurring infinitely often at irrational ratio, uniform bounds 0 < a ≤ βω_k ≤ b, cutoffs D_k ≥ 2 ⟹ the tower’s eigenvalue family satisfies the III₁ fingerprint — PLUS the hypothesis-free alternating {1, √2} qubit instance via irrational_sqrt_two. The operator reading rests on three facts cited verbatim and never proved (Araki–Woods 1968; Connes 1973); no von Neumann algebra is constructed anywhere in the development.
• T4 — the Powers guard (gibbsTower_constant_not_fingerprint): a constant-frequency tower provably FAILS the fingerprint (every tail exponent lies in sℤ — the arithmetic fingerprint of the Powers factor III_e^{−s}, cited). The separation theorem: the predicate is neither vacuous nor universal.
• T5 — the state limit (gibbsLimitMeasure): the σ-additive infinite-mode Gibbs measure on occupation configurations — the unique projective limit of the dynamics campaign’s own thermal marginals through the held Kolmogorov/product machinery, whose finite marginals ARE the code’s DY Gibbs weights.
• T6 — non-atomicity (gibbsLimitMeasure_noAtoms): under the uniform frequency bound every singleton configuration is null (the cylinder squeeze) — so no diagonal-density quantum reading of the limit exists: FALSE, not deferred; the Type-I shortcut is provably closed. The vacuum-atom dichotomy is cited, never proved.
• T7 — the finite operator tower (cornerEmbed): for nested corners C ⊆ C′ the inclusion is a unital ⋆-homomorphism, mode-compatible, state-compatible (φ_C′∘ι = φ_C), and modular-flow equivariant (σ_s^C′∘ι = ι∘σ_s^C, via the kappaOf eigen-law) — a family of finite-dimensional maps only: exactly the ITPFI tower DATA, its classification never performed.

The closure (C1–C11): the von Neumann double-commutant theorem

The convergent blocker of the continuum program — the missing lemma that four separately-named frontiers all reduce to — is now a machine-checked theorem, in Mathlib-styleable form: Mathlib defines VonNeumannAlgebra by the bicommutant property but has no bicommutant theorem; this campaign closes that gap (QIQTH/VonNeumann/; axiom-free, std-3; all eleven increments landed, the stretch included).

• THE CENTERPIECE (vonNeumann_double_commutant, green first try): for every unital ⋆-subalgebra A of the bounded operators on a complex Hilbert space, the double centralizer A″ equals the set of operators approximable from A in norm on every finite tuple of vectors — the SOT closure, stated concretely (SOTApprox; one approximant per tuple, the load-bearing quantifier order). Forward: the classical amplification argument fully verified — the cyclic-subspace projection in the commutant (⋆-closure load-bearing, upper-triangular counterexample), single-vector density (unitality load-bearing, A = {0} counterexample), the frozen PiLp amplification interface (ι† = π), the two minimal matrix-commutant lemmas (never Mₙ(A′)), n-vector density. Converse: the (x, Sx) two-vector estimate — single-vector approximability is provably insufficient.
• The WOT stretch (wotClosure_image_eq_image_bicommutant, shipped): the weak-operator closure IS the bicommutant, wholly inside Mathlib’s WOT type copy (separate continuity only — joint WOT continuity of multiplication is false). With the centerpiece: WOT closure = SOT closure = A″ — the full classical statement.
• VonNeumannAlgebra.generatedBy — the vN algebra generated by any operator set (double centralizer + minimality + the Galois lemma), proven to BE the SOT closure of the generated ⋆-algebra (generatedBy_carrier_eq).
• The two payoffs, honestly scoped: crossedProductVN — the crossed product M⋊_σℝ packaged as a genuine VonNeumannAlgebra on L²(ℝ;H) with the membership characterization (packaging only; the dual-weight trace is NOT claimed to extend to the weak closure); and limitVN — the directed-union limit algebra for any hypothesized common representation (the refinement-tower limit; the code tower’s own instantiation awaits the tower-GNS campaign).

The representation (R1–R9): the tower’s limit von Neumann algebra exists

The GNS construction of the compatible Gibbs family: the corner tower — previously a family of finite matrix algebras related by embeddings — now acts on ONE Hilbert space, and its directed-union limit von Neumann algebra is an actual, named, axiom-free object (QIQTH/TowerGNS/; the first genuinely infinite-dimensional quantum object of the development).

• The Hilbert space TowerGNS — the completion of the direct sum of ALL finite corners under the stabilized Gibbs pairing, which is deliberately semidefinite: the null directions are exactly the direct-limit gluing, and the metric completion performs the identification (towerGerm) — no quotient is ever taken. Instance architecture = Mathlib’s own GelfandNaimarkSegal.lean, verbatim.
• The representation towerRep — every corner algebra acts as a unital ⋆-algebra homomorphism (bounded via an elementary Frobenius estimate — honest scope: bounded, NOT claimed contractive), with the algebra laws holding ONLY in the completion (provably false at the pre-level — the stages differ; the germ reconciles). CAPSTONE towerRep_cornerEmbed: π_C′ ∘ ι = π_C — the tower acts coherently through every stage.
• The cyclic vector Ω — implements EVERY corner Gibbs state as a vector state (⟪Ω, π_C(a)Ω⟫ = φ_C(a)) and its orbit is dense. Ω is NOT shown separating.
• ★ towerLimitVN ★ — the directed-union limit von Neumann algebra of the representation images (the double-commutant campaign’s limitVN, instantiated), with membership characterized by SOT-approximation from the finite stages, and the ℕ-instantiation freqTowerLimitVN for the code’s frequency tower. The object THE TOWER and THE CLOSURE campaigns were built for.

The transport + the accounting: dynamics for the limit algebra; the species form forced

Two tracks, one campaign (all axiom-free, std-3, budget 0).

• THE MODULAR TRANSPORT — the per-corner Gibbs modular flows transported to towerFlow, a strongly continuous one-parameter unitary group U_t on the tower GNS space: U₀ = 1, the group law, U_t* = U_−t, U_tΩ = Ω, THE IMPLEMENTATION THEOREM U_t π_C(a) U_−t = π_C(σ_ta) at every finite stage (the covariance is exact already at the pre-level), and towerLimitVN invariant under conjugation by the flow. The finite-stage boundary KMS identity is displayed on the limit space (honestly bannered: not strip analyticity, not a KMS state of the limit algebra). HAVE NOT: no Tomita Δ/J, Ω not shown separating, no Stone generator (the named next hook), no type classified — U_t is defined by transport.
• THE ACCOUNTING — the honest maximal species upgrade: the regulator rigidity theorem (any positive, species-additive, monotone, rescaling-covariant family is forced to the Sakharov/Dvali form 1/G = N_eff·Λ², the exponent an output, with a counterexample showing weakened covariance breaks it); the first derived — not cited — heat-kernel coefficient in the repository (1/√(4πt) from Mathlib’s Gaussian integral); and the mixed-species consistency chain — one shared species datum feeds both the entanglement entropy and the induced 1/G, with the mixed-content 1/4 and S = A/4G as theorems (the entire species sum cancelling), chained through the BTZ Cardy count. HAVE NOT: the numerical value of G is not derived; the c_i stay cited Seeley–DeWitt data — a consistency chain over one shared cited datum, NOT an independent cross-check.

The generator: the self-adjoint Hamiltonian of the limit dynamics, computed

towerGen := stoneGen (towerFlow) — the transported flow’s genuine self-adjoint unbounded generator (K = K†), instantiating the held Stone theorem with the five flow facts (two adapter lemmas; every increment green on first or second build). With it:

• The zero-mode — Ω ∈ dom(K) and KΩ = 0: the cyclic vector is annihilated because the flow fixes it exactly.
• The explicit core — on every pure component, K ↑(of_C a) = ↑(of_C [H_C, a]) with H_C = diagonal(log gibbsWeight): the finite-stage modular Hamiltonian acts by commutator; the generator is COMPUTED, not just certified, on a constructively dense domain (no Gårding mollification).
• Flow covariance — U_s preserves dom(K) and K U_s = U_s K.

The separation: Ω is cyclic AND separating — the standard form

The limit algebra reaches the standard-form hypothesis pair of Tomita–Takesaki theory, axiom-free (RightMul.lean, Separation.lean):

• The weight exchange + half-power intertwining — T7’s modular-frequency lemma exponentiated gives ι(a)·√ρ_K = √ρ_K·ι(rightConj a), so RIGHT multiplication is bounded with the weighted Frobenius constant Σ‖a_nm‖²(w_m/w_n) (never claimed contractive).
• The commutant facts — left and right actions commute (deep-stage double germ; no Finset equality ever stated), and every element of towerLimitVN commutes with every right multiplication by pure bicommutant algebra (double-centralizer membership is definitional).
• ★ towerCyclicVec_separating ★ — T ∈ towerLimitVN, TΩ = 0 ⟹ T = 0: T kills the right orbit of Ω, which IS the left orbit, and that orbit spans densely. With the held cyclicity: Ω is CYCLIC AND SEPARATING for the tower limit von Neumann algebra. Plus towerLimitVN_eq_of_apply_cyclicVec — the well-definedness germ of a future Tomita S₀.

The Tomita operator: S₀, computed and closable

Modular theory proper begins: towerTomita₀ — the Tomita operator of the tower limit state on its classical orbit domain, as a genuine conjugate-linear (σ-semilinear) partial operator:

• Well-defined because Ω is separating (the previous campaign’s capstone doing its job); involutive; densely defined; S₀Ω = Ω; and the computed core action S₀ ↑(of_C a) = ↑(of_C aᴴ) — the Tomita involution is conjugate-transpose on pure components.
• The finite σ₋ᵢ, computed — the commutant-side right multiplications carry the exact adjoint R_a† = R_{ρaᴴρ⁻¹} (the engine squared + the modAut bridge): the honest finite-tower substitute for KMS analyticity, a theorem rather than an analytic continuation.
• The classical pairing ⟪T*Ω, R_aΩ⟫ = ⟪R_a†Ω, TΩ⟫ on a dense family, and closability in the graph-limit sense (T_nΩ → 0 ∧ T_n*Ω → v ⟹ v = 0).

The conjugate closure: S̄ as an object — and a new slice of Mathlib

The closure of the Tomita operator exists, built by the ℝ-reduction (a conjugate-linear map IS ℝ-linear; Mathlib’s closure theory applies verbatim through the global complexToReal instances — no local instances anywhere):

• Four new abstract theorems (Mathlib-only imports — upstream-gap contributions): the ℝ-restriction view of a conjugate-linear partial map; the sequence-closability bridge (isClosable_of_seq — absent from Mathlib even for ordinary linear maps); and the transfer theorems — conjugate-homogeneity and the involution survive closure (no adjoint anywhere).
• towerTomitaBar — S̄: closed, extending S₀ with the orbit domain as a core, S̄Ω = Ω, conjugate-transpose on pure components, twist-guarded conjugate-homogeneous, and fully involutive with trivial kernel and range = domain.

The modular operator: Δ, computed as the modular automorphism

The campaign after the conjugate closure delivers Tomita–Takesaki’s central object for the tower limit state:

• Tomita’s F with no Riesz machinery — the conjugate-linear adjoint of S̄, built on the ∃-Riesz domain {y : ∃ w, ∀ x, ⟪S̄x, y⟫ = ⟪w, x⟫}: no real inner product, no dual-space machinery, no completeness argument anywhere. The abstract conjAdjoint (closed in the sequence sense, with the core-extension equalizer lemma) is itself a Mathlib-gap contribution.
• Δ := F∘S̄ — a ℂ-linear densely defined partial operator (the two conjugations cancel): symmetric (IsFormalAdjoint Δ Δ), positive (⟪Δx, x⟫ = ‖S̄x‖² ≥ 0), closable (Δ ≤ Δ† with Δ† closed), fixing Ω.
• The computation — on the dense pure-component core, Δ ↑(of_C a) = ↑(of_C (modAut_ρC a)): the continuum modular operator acts as the finite modular automorphism ρaρ⁻¹, stage by stage — the modular operator of the physics, computed rather than postulated.

The von Neumann campaign: Δ† = Δ — and von Neumann’s theorem itself

One campaign later, the modular operator is genuinely self-adjoint (six increments in a single session, four consecutive first-try greens):

• Three abstract Mathlib-gap files (RCLike-generic, Mathlib-only imports): the self-adjointness kernel (symmetric + ran(1+A) = ⊤ ⟹ A† = A); the von Neumann graph orthogonal decomposition of a closed partial operator in ℓ²(E×E) (no adjoint anywhere); and von Neumann’s theorem itself — T†T densely defined and self-adjoint for closed densely defined T, over any RCLike field. None exists in Mathlib at the pin.
• The i-twist — conjugate-homogeneity upgrades the real graph-orthogonality pairing to the full complex pairing, which lands verbatim in the ∃-Riesz F-domain membership: ran(1+Δ) = ⊤.
• The headline — Δ† = Δ (towerModularOp_isSelfAdjoint): the tower modular operator is a genuinely self-adjoint, positive, closed, densely defined operator fixing Ω and computed as the finite modular automorphism on the dense core; with kernel triviality and the resolvent bound ‖x‖ ≤ ‖x + Δx‖.

The resolvent campaign: Δ^{it} exists

The modular unitary group of the tower limit state is constructed (seven increments, every one first-try green):

• The resolvent — R := (1+Δ)⁻¹, an everywhere-defined self-adjoint contraction with 0 ≤ R ≤ 1, trivial kernel, dense range = dom Δ, spectrum in [0,1], RΩ = ½Ω, and the exact identity Δ∘R = 1−R — Δ is a function of a single bounded self-adjoint operator.
• The abstract PVM supplement (reusable) — the operator-level spectral theorem T = ∫λ dE; the kernel-atom lemma (injective self-adjoint T forces E({0}) = 0 — not automatic from kernel triviality); the eigenvector calculus f(T)x = f(r)x.
• The headline — Δ^{it} := towerModUnitary, the bounded Borel calculus of R under the symbol ((1−r)/r)^{it}: a strongly continuous one-parameter unitary group (U₀ = 1, U_{s+t} = U_sU_t, U_t⋆ = U_{−t}) fixing the cyclic vector (U_tΩ = Ω), commuting with Δ on its whole domain, with E({0}) = 0 certifying the group genuinely represents δ^{it} on the spectrum.

The identification: the exponential-recovery wall, crossed — and Tomita I

The campaign after the resolvent identifies the two unitary groups (five increments, every one first-try green):

• The eigenvector route — the Gibbs density is diagonal by construction, so matrix units are simultaneous eigenvectors of the finite modular automorphism (modAut ρ (e_nm) = (w_n/w_m)e_nm), of Δ, of the resolvent, and — through the eigenvector calculus — of Δ^{it}, with the same explicit scalar e^{it(log w_n − log w_m)} the transported physical flow carries. No spectral theorem, no Stone uniqueness, no log Δ needed anywhere.
• The identification — towerFlow = Δ^{it} as operators (towerModUnitary_eq_towerFlow): the transported physical dynamics of the tower limit state IS the spectral modular flow of its modular operator; corollary, towerGen IS the Stone generator of Δ^{it}.
• Tomita’s theorem, first half — Δ^{it} implements the modular automorphisms (Δ^{it} π(a) Δ^{−it} = π(σ_t a)) and preserves the limit algebra: Δ^{it} towerLimitVN Δ^{−it} = towerLimitVN — the modular theory of the physics equals the modular theory of the state.

Reproduce the verification

~/.elan/bin/lake build QIQTH
~/.elan/bin/lake build QIQTH.AxiomAudit   # emits #print axioms for every theorem

Each theorem reports depends on axioms: [propext, Classical.choice, Quot.sound]. The full statement-level index lives in the repository; a companion formalization paper is in preparation.

A note on wording: “no axioms” here means no project axioms. propext, Classical.choice, and Quot.sound are the standard classical foundations every ordinary Mathlib proof uses; we keep them and add nothing of our own.