The mathematics

The theory

The framework has four moving parts: a capacity axiom, a cost functional for regional information, a conjecture that ties two records to an overflow of that capacity, and a conditional theorem that draws the single-world conclusion. Only the cost functional’s underlying calculus is machine-verified; the rest is stated honestly as postulate, conjecture, or open.

1. Finite regional capacity (FQ)

A bounded region RR with boundary area AA carries a finite information capacity

QR  =  A4P2,Q_R \;=\; \frac{A}{4\ell_P^2},

the holographic / Bekenstein–Hawking bound, with AA the boundary area of the region and QRQ_R in natural entropy units (divide by ln2\ln 2 for bits). In QIQT-H this enters as a postulate about physically instantiable content, not merely about thermodynamic entropy: the renormalized information of any state the region actually realizes obeys SrenQRS_{\mathrm{ren}} \le Q_R. Grounding this bound from a more primitive principle, and stating it cleanly in the continuum, is one of the open problems.

2. The cost of regional content: χR\chi_R

To compare “how much information” two regional states carry, QIQT-H uses the Araki relative entropy S(ωω0)S(\omega \,\|\, \omega_0) of a state ω\omega against a reference ω0\omega_0 (the local vacuum). For a bounded region the local algebra is not the familiar Type I factor of ordinary quantum mechanics; in relativistic field theory it is a Type III1_1 von Neumann algebra. Araki relative entropy is already well defined there. The Type II “dressed” algebras — which carry a trace-like generalized entropy — come from the gravitational crossed-product construction of Chandrasekaran–Penington–Witten and Witten; QIQT-H borrows that picture as motivation, it is not something established here. The regional cost functional is

χR(ω)  =  S(ωω0),\chi_R(\omega) \;=\; S\big(\omega \,\|\, \omega_0\big),

computed through Tomita–Takesaki modular theory: the modular operator Δ\Delta, the modular conjugation JJ, and the modular flow Δit\Delta^{it} of the reference state. (Identifying this vacuum-relative distinguishability functional with the cost to instantiate regional content is itself part of the QIQT-H hypothesis, not a theorem.) For coherent excitations W(f)ΩW(f)\Omega of a free field this reduces to an explicit one-particle expression, the Casini–Grillo–Pontello entropy SCGP(f)S_{\mathrm{CGP}}(f), and this coherent-state reduction is what the Lean development checks, end to end, from the bounded modular operators to the entropy-reduction identity.

Scope. What is verified is the modular and relative-entropy calculus for the free-field coherent sector, the bookkeeping machine for χR. The verified part does not include the Type II regional construction itself, the (FQ) axiom, or the conjecture below.

3. The crux: macroscopic definiteness (H2)

Here is the load-bearing physical claim. Let a “record” be a stable, redundantly-copied, macroscopically distinguishable pointer state of the form decoherence leaves behind. The Macroscopic Definiteness Conjecture states:

A regional state carrying two or more distinct macroscopic records has χR\chi_R exceeding the capacity QRQ_R of any region that would have to host it.

This is the step that does the real work, and it is a conjecture. It asserts that the information cost of genuine macroscopic multiplicity is not merely large but specifically larger than the holographic ledger allows. One subtlety is load-bearing: the cost in this inequality need not be the same χR\chi_R the Lean development computes. A plain relative-entropy or data-processing estimate of two readable records yields only about log2\log 2 of classical information, not an area-scale QRQ_R. The conjecture is precisely that the right instantiation cost of genuine macroscopic multiplicity is area-scale — and identifying that cost measure is itself part of the problem. Establishing H2, even in a model, is the central open problem.

4. The conditional theorem: single record

Granting (FQ) and the conjecture, the conclusion follows as a conditional theorem. If a 2\ge 2-record state cannot be instantiated in RR, then the only regional content compatible with the bound is single-record. After decoherence has stabilized and proliferated the records, the per-run state the region realizes is therefore one definite macroscopic world, with no collapse term added to the global dynamics.

This is worth stating carefully, because “one outcome” and “unitary evolution” sound contradictory. The global wave function evolves unitarily throughout; what the finite-capacity constraint does is render multi-record regional content inadmissible. Which single admissible record is the actual one is then a selection among the unitarily-evolved alternatives, not a dynamical modification of the Schrödinger equation — the (Φ, λ) account. Making that selection precise, and deriving its statistics, is the dynamical-realization and Born problem below.

Two honest caveats. First, the theorem as formalized is a static exclusion: it says two-record content is not instantiable, not yet that the unitary dynamics drives an initial superposition to a single realized record. Closing that “dynamical realization” gap is open. Second, the theorem yields that there is one outcome, not which, and with what frequency.

5. Born statistics

That outcome kk occurs across runs with frequency ck2|c_k|^2 is the Born rule. QIQT-H aims to recover it from typicality: over the measure of microscopic initial conditions compatible with a given preparation, the realized single-record outcome has frequency ck2|c_k|^2 for typical initial data. A Lorentz-covariant such measure for free fields is the linchpin, and it is open. Born statistics are not assumed, but they are not yet derived either.


The four-link status, at a glance: (FQ) postulate · χR\chi_R calculus machine-verified · H2 conjecture the crux, open · single record conditional theorem (+ dynamical-realization gap) · Born open. The formalization page documents exactly which pieces are checked; the open problems page lays out the four gaps and what each one buys.