Machine-checked substrate

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).

Scope. What is verified is the standard borrowed mathematics, Tomita–Takesaki modular theory and Araki relative entropy in the free-field coherent sector, not the dressed Type II regional framework, the holographic axiom (FQ), the Macroscopic Definiteness Conjecture, or Born-from-typicality. It strengthens the floor the argument stands on; it does not close the open problems.

The headline result

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

\frac{d}{dt}\Big|_{0}\,\big\langle\Omega,\ \Delta_{W(f)\Omega\,\mid\,\Omega}^{\,it}\,\Omega\big\rangle = -\,i\,S_{\mathrm{CGP}}(f),

so that

S_{\mathrm{Araki}}\big(\omega_{W(f)\Omega}\,\Vert\,\omega_\Omega\big) = S_{\mathrm{CGP}}(f) \ge 0.

Index of machine-checked results

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

Finite Araki relative entropy

theorem	statement
`arakiEntropy_eq_relEntropy`	$S_{\mathrm{Araki}}(\rho\Vert\sigma)=\operatorname{tr}\rho(\log\rho-\log\sigma)$ (Umegaki)

Bounded Tomita–Takesaki (standard subspace)

theorem	statement
`modConj_rvdRC_modConj`	$JRJ=2-R$
`modConj_rvdT_of_mem_K`	$J(T\xi)=(2-R)\xi$ for $\xi\in\mathcal{K}$
`modUnitary`	$\Delta^{it}$ : group law, unitarity, strong continuity

One-particle CGP relative entropy

theorem	statement
`cgpEntropy`	$S(\xi)=-\!\int\log((2-r)/r)\,d\mu^R_\xi$
`rvdSpec_balance`	the CGP spectral balance
`cgpEntropy_nonneg`	$S(\xi)\ge 0$ for localized $\xi\in\mathcal{K}$

Free-field (Fock) modular flow

theorem	statement
`secondQuantModFlowH`	$\Gamma(\Delta^{it})$ : one-parameter group, vacuum-fixing, strongly continuous on coherent vectors
`secondQuantModFlowH_weylH`	$\sigma_t(W(u))=W(\Delta^{it}u)$

Coherent-state relative modular operator and reduction

theorem	statement
`relModFlowH`	$\Delta^{it}_{W(f)\Omega\mid\Omega}=W(f)\,\Gamma(\Delta^{it})\,W(f)^{*}$
`connesCocycleH_chain`	$[D\omega_{W(f)\Omega}:D\omega_\Omega]_t=W(f)W(-\Delta^{it}f)$ + chain rule
`hasDerivAt_relModFlow_vacuum`	$S_{\mathrm{Araki}}(\omega_{W(f)\Omega}\Vert\omega_\Omega)=S_{\mathrm{CGP}}(f)$

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.