A bounded spacetime region has only finite operational information capacity — a postulate motivated by gravitational entropy bounds. QIQT-H conjectures that this forbids it from instantiating two macroscopically distinct records at once, so after decoherence the per-run actual content is single-record, with no collapse term added to the dynamics. Whether that conjecture holds is the open crux.
sorry · reproducible The whole thesis is one chain. Two links are postulates, one is the machine-verified mathematical substrate, one is a conditional theorem, and one is open. Each is labelled honestly.
Honesty is the point. The Lean development verifies the standard modular and relative-entropy calculus underlying the regional cost , not the holographic axiom, not the central conjecture, not the Born rule.
| Component | Status |
|---|---|
| Araki relative entropy = Umegaki (finite case) | machine-checked |
| Bounded Tomita–Takesaki: , , , strong continuity | machine-checked |
| One-particle CGP relative entropy + positivity | machine-checked |
| Free-field modular flow , | machine-checked |
| Coherent-state relative modular operator, Connes cocycle, entropy reduction | machine-checked |
| Holographic capacity axiom (FQ): | postulated |
| Macroscopic Definiteness Conjecture (H2) | open · the crux |
| Born statistics from typicality | open |
The measurement problem, finite information, and single outcomes, in plain language.
Start here →The (FQ) axiom, , Type II algebras, and the conditional single-record theorem.
Read the math →Constitution and actuality: the global wave function, and which admissible record is real.
The picture →The Lean 4 / Mathlib machine-checked substrate, theorem index, reproducible build.
See the proofs →The four gaps between a research program and a theory, and what closing each buys.
The frontier →