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 with boundary area carries a finite information capacity
the holographic / Bekenstein–Hawking bound, with the boundary area of the region and in natural entropy units (divide by 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 . 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:
To compare “how much information” two regional states carry, QIQT-H uses the Araki relative entropy of a state against a reference (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 III 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
computed through Tomita–Takesaki modular theory: the modular operator , the modular conjugation , and the modular flow 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 of a free field this reduces to an explicit one-particle expression, the Casini–Grillo–Pontello entropy , and this coherent-state reduction is what the Lean development checks, end to end, from the bounded modular operators to the entropy-reduction identity.
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 exceeding the capacity 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 the Lean development computes. A plain relative-entropy or data-processing estimate of two readable records yields only about of classical information, not an area-scale . 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 -record state cannot be instantiated in , 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 occurs across runs with frequency 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 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 · 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.