Φ and λ — constitution and actuality
There is an apparent paradox at the heart of the conditional theorem: the global dynamics is unitary, yet each run yields one outcome. Unitary evolution and a single result sound incompatible — it is exactly the tension that pushed the textbook to a collapse postulate and pushed Everett to many worlds.
QIQT-H aims to dissolve it — not with a new law, but by separating two questions the measurement problem usually runs together: what is constituted and what is actual. The first is answered by , the second by . To be honest about it, this relocates the tension into rather than making it vanish; whether the relocation succeeds turns on the open problems below.
Φ — the global wave function constitutes everything
is the universal state. It evolves unitarily, always; there is no term in its dynamics that collapses it, and there is no observer standing outside it. Apparatus, environment, record, and experimenter are all patterns within — there is no external vantage from which a measurement is performed on it.
This is the literal reading of the formalism taken seriously: the observer is the wave function. What we call “an observer” is a macroscopic, decohered, redundantly-recorded substructure of — the very kind of record the theory is about. We do not look at from outside; we are realizations of it.
λ — which admissible record is actual
The unitarily-evolved offers several mutually-exclusive macroscopic records; marks exactly one as actual. Decoherence first makes those records non-interfering and redundantly objective — but that removes interference, it does not make one of them actual. The single actual record is ‘s doing.
Correction (2026). An earlier version said the finite capacity itself forbids two actual records (their classical contents “would together exceed the budget”). That is a category error: the holographic bound counts independent degrees of freedom, not a sum of redundant classical records, and ordinary record entropy is capped at ~A3/4 (~1091) far below the bound (~10122) — a permanent ~31-order gap. So capacity does not exclude a second actual record; “two actual records can’t coexist” reduces to a classical carrier holding one value, which is itself supplied by λ. Qmax’s honest role is the finite record stage (how many distinguishable records exist, ), not the single-outcome selection.
is the selection of which admissible record is the actual one. It is the move the textbook misnames “collapse” — but here it is not a dynamical event. adds nothing to the Schrödinger equation, exerts no force, and leaves untouched. It is a fact about which of the constituted, unitarily-evolved alternatives we find realized, not a physical process that edits the state.
Two layers. Φ is constitution — what there is, evolving unitarily. λ is actuality — which admissible record obtains. This is one dynamical law plus an actuality postulate, not a cost-free relabeling: keeping the layers apart is what lets “exact unitarity” and “one outcome” coexist, but giving λ a precise, dynamically-consistent form is still open.
No fundamental probability, no chooser
is not a random draw made by a privileged agent, and it is not an extra stochastic law bolted on. There is no fundamental chance and no fundamental choice in QIQT-H. Probability is meant to emerge: across many runs, the actual records distribute with frequency for typical microscopic initial conditions. What looks like a probability is the typicality of which realization a record like us finds itself to be — not a die that rolls. For the plain-language account of how this yields , see How the Born rule emerges.
That this typicality reproduces the Born weights is not yet derived; it is the Born-from-typicality problem. And it carries a real risk of circularity: until the typicality measure — over uncontrolled microscopic initial conditions, or over admissible -histories — is specified independently of the Born weights, this is a target, not a derivation. Likewise, making precise as a selection compatible with the unitary dynamics — that exactly one admissible record obtains, not zero, and that the admissible space is dynamically invariant — is the dynamical-realization problem. The ontology here is coherent; these pieces of it are open.
How far this is pinned down. The Born-from-typicality claim above is backed by a machine-checked reduction (the Born-rule formalization paper): records give definite outcomes but no weights; among rules p ∝ f(w), refinement-additivity, no-signalling under remote refinement, and Born are equivalent; and a no-go proves the squared-weight family w2 obeys every Born-free premise — so an extra principle is unavoidable, which is the circularity worry made precise rather than waved away. A finite H-theorem then reduces the residual to a Born-agnostic typicality postulate (reversibility over a uniform bath, plus mixing) instead of to |Ψ|2 itself. It sharpens the open problem; it does not yet close it.
The λ construction, made precise
Stated sharply, is a single sample from a Lorentz-covariant probability law on record histories — four pieces:
- Stage — the causal-diamond poset; for each region a finite set of decohered, redundantly-broadcast candidate record alternatives (not yet “actual”). The capacity bound is posited to limit their number — an actuality-layer assumption, not something the holographic entropy bound proves on its own.
- Histories — compatible global assignments (one record per region, agreeing on overlaps), each a complete 4D history with no preferred time-slice.
- Law — the Born weight (Born is input here), -additively extended, and covariant as a law: .
- λ — one history drawn from .
The key move: a covariant measure is not a covariant selector. Just as the rotation group has an invariant measure on the sphere but no invariant point, the law is Poincaré-covariant while a sampled generally is not a fixed point of the symmetry — ordinary sample non-invariance, not a hidden preferred frame. So need not be (and cannot be) an equivariant function of ; it is a contingent draw.
Now machine-checked (free-field sector). For the 1+1D free field this covariant Born law is verified in Lean: a σ-additive measure exists (finite-fiber Kolmogorov extension — the finiteness is the capacity bound), it is the same in every Lorentz frame, and it satisfies the decoherent-histories consistency condition Re D(α,β) = 0 exactly (this is what makes the Born weights obey the probability sum rules). For orthogonal records the full off-diagonal D = 0 (strong), with an exact overlap-correction formula off orthogonality and a redundancy law by which broadcasting drives D → 0 (Quantum Darwinism). See the theorem index. Born itself remains an input, not a derivation.
Realm selection (the “metaselector”) — now a machine-checked trilogy. Picking which record framework is actual (the realm) is the classic decoherent-histories gap (Dowker–Kent). It is now resolved as a no-go trilogy plus a positive selector, all machine-checked: capacity does not select it (distinct capacity-maximal realms exist), symmetry/typicality does not (the unitary group acts transitively on frameworks, so any invariant score is constant — closing the “most typical framework” route), and the state Φ alone does not (a single projection generates only the trivial ). What does select it is einselection — Zurek’s commutativity criterion: a record commuting with the monitored observable commutes with the interaction , so it is decoherence-free. Einselection presupposes a system–environment cut (the residual Dowker–Kent input) — so the metaselector is the interaction Hamiltonian, reduced to that cut, not derived from nothing. This whole layer is verified scaffold: stays inert, so the scheme remains operationally Everett. See the theorem index.
The finite-information core — only one construction survives. Where can λ’s finiteness actually live? There is a machine-checked dividing line. Finiteness in the actuality domain works: λ is a finite index over a finite set of record-histories, carrying the exact Born weights (a real number computed from Φ, not rounded). This is Born-transparent — it preserves the marginals (operational no-signaling) and equal weights (Zurek envariance). The tempting alternative — putting the finiteness in the probability law (a “grid” that rounds the weights to a finite resolution) — provably fails: it breaks the program’s own envariance and no-signaling, and is retired. So there is exactly one viable finite-information λ: the finite index with exact Born. The holographic budget then bounds the index cardinality (how many distinguishable record-histories, ) via the mutual-information identity — λ’s information is the record information it indexes, no new beable. The one/two/three-qubit “universes” in the Lean development are the concrete toys of this construction. Honest caveat: because it keeps Born exact, this finite-information λ is still operationally Everett — finiteness is “Quantized Information” made honest (the actual record-history is a finite object), not a route to out-predict Everett.
The λ-selection schema, now machine-checked
What was, a year ago, a bare actuality postulate is now a verified consistency-and-selection schema — machine-checked (Lean 4 / Mathlib, axiom-free) at the finite, the one-particle continuum (the bounded modular flow ), and the second-quantized free-field (, a unitary group) levels. We say schema, not law, deliberately: “axiom-free in Lean” means no extra Lean axioms, not no physical postulates — those sit in the hypotheses (a chosen record context, exact decoherence, the Born weights, a uniform seed measure). The crossed-product “Type II dressing” idea for λ is retired as a category error; λ rides the standard form and the modular automorphism (the records are atoms of a chosen abelian coarse-graining associated with the Type III algebra, not atoms of the factor — it has none). What is verified:
- Which records (kinematics). Which record context admits a state-preserving coarse-graining is fixed by Takesaki’s criterion — invariance under the modular flow, i.e. , exact decoherence. The dephasing map is then the state-preserving conditional expectation onto the (generally nonabelian) block-diagonal algebra; the classical record labels are the atoms of the abelian sub-coarse-graining. (The state here is faithful/reduced, not the global pure ; exact is an idealization.)
- Born weights. Each record’s weight is the algebraic state value — via the natural cone / vacuum state, no trace — and over a record family these are a genuine probability (on the Fock vacuum state the single-mode Weyl-bit effect gives ).
- Modular invariance (not physical dynamics). The dephasing map commutes with the modular flow for all — no modular recoherence inside the chosen invariant record algebra. This is a genuine consistency fact, but the modular flow is not the physical Hamiltonian evolution (they agree only in special KMS / Bisognano–Wichmann cases), so it is not a proof that actual records never recohere under the real dynamics.
- The selection event (a sampling representation). An explicit inverse-CDF constructor takes an actuality “seed” to exactly one record (totality + uniqueness of a sampling map), and the single-shot seed measure of a record equals its Born weight. It adds no actualization mechanism, and a single-shot measure is not yet an across-run frequency (that needs a product measure + a law of large numbers).
What this is, honestly. Because λ has no back-reaction and the Born weights are assumed, the scheme is operationally equivalent to standard (Everettian / orthodox) quantum mechanics — λ is unobservable, and it makes no prediction beyond Born statistics. Its content is interpretive: a single actual record by stipulation, no collapse, no second substance — the modal / Everett-plus-actuality-tag family. The constructor reduces the whole selection to one datum — which seed is actual — and that seed is λ: the single primitive a non-dynamical single-world theory must take as given (its dynamical origin is not derived, and arguably cannot be). What is left is either provably irreducible (the seed; the strong Born premise) or genuine multi-year mathematics (the Haagerup natural-cone existence; the interacting case). The honest next content-adding targets are a global decoherent-history selector (one coherent world, not one atom of one finite resolution) and an explicit across-run frequency theorem.
How this differs from the usual answers
- Collapse interpretations make the selection a dynamical event that breaks unitarity. Here is not dynamical and breaks nothing; stays exactly unitary.
- Many-worlds keeps every decohered branch as an existing world. Here the unselected components of are not actual worlds: a region admits only one macroscopic record, so the alternatives are mutually-exclusive candidates for actuality that remain unactualized, not coexisting worlds.
- Bohmian mechanics adds hidden particle trajectories as the actual configuration. In the broad (Bell / modal) sense is also an extra actuality variable beyond — but it is not Bohmian: it is a record-valued selector over decoherence-defined alternatives, not a trajectory in configuration space.
What λ adds to Everett — and what it doesn’t. QIQT-H shares Everett’s dynamics exactly: is the same unitarily-evolving wave function. What pure Everett deliberately lacks is an actuality selector — every branch is equally real, with no fact about which is “the” actual one. is that fact, so QIQT-H is a genuinely different, single-world interpretation (not many-worlds). Three honesties keep this from overclaiming. (i) The difference is ontological, not empirical: is inert (no back-reaction, unobservable), so QIQT-H is operationally identical to Everett — it makes no new prediction. (ii) Positing a selector is not new: it is the modal family’s move (Kochen–Dieks, Bub) and structurally Bohm’s (the particle configuration as the actuality), so the idea of an actuality tag is not ours. (iii) What is ours is the verified selection schema: machine-checked kinematics including what fixes the record framework — einselection, via the metaselector no-go trilogy (neither capacity, nor symmetry, nor the state selects it) — while ‘s actual value (the seed) and the typicality measure remain the two open primitives. So we define the selector’s structure; we do not derive . “More than Everett” therefore means a different (single-world) ontology with a machine-checked selection schema, not a theory that out-predicts Everett — which is exactly why we keep saying “operationally = Everett.”
Locality and Bell — and why this is not superdeterminism
A single-world ontology has to face Bell. To be explicit: QIQT-H is Bell-nonlocal — like every single-world theory that reproduces quantum statistics, the global law on violates Bell local causality (). No-signalling and microcausality do hold, but those are weaker, operational constraints; they do not rescue local causality, and treating them as if they did would be a category error.
What QIQT-H is not is superdeterministic: it does not correlate the measurement settings with , and it does not deny measurement independence. The Bell correlations come from the nonlocal global state — entanglement — exactly the source they have in Everett, together with a contextual actuality selection (which record is actual can depend on what is actually measured). Assigning values only to the records that are actually decohered in the actual context is also what dodges Kochen–Specker / Fine (no noncontextual value-map over all counterfactual settings) — but it does not make Bell go away; the model is irreducibly global/contextual. The settings stay free; the price for Bell is contextuality and a global consistency condition on across overlapping regions, not a conspiracy between past and future. The one place superdeterminism could sneak in is the typicality measure — so it must be over the uncontrolled microstate in the ordinary, setting-independent sense (as in Bohmian quantum equilibrium or Everett typicality), never a measure tuned to the settings.
Honest scope
This page is the interpretive layer of QIQT-H, and the reading of the machinery — what a single world is — is more speculative than the machine-verified substrate. But is no longer just a picture: as recorded above, its kinematic criterion, modular-invariance, Born-weight bookkeeping, and inverse-CDF selection are machine-checked (finite through free-field, axiom-free) — a verified consistency schema, not a derived law, and conditional on a primitive seed and a Born premise. What stays genuinely open is the dynamical origin of the actuality datum (the seed, which is λ itself; arguably irreducible for a non-dynamical selector), an across-run frequency theorem, and the cited continuum walls beyond the free field. Treat the ontological reading as the program’s proposed picture; treat the schema as verified where it can be — around an admitted primitive.
In the broad hidden-variable sense, is an additional actuality variable beyond — but it is not a local, noncontextual preassignment of all outcomes. A completed version must define only on decoherence-selected record algebras, keep it consistent across overlapping regions, recover the Bell correlations without signalling, and justify a typicality measure not secretly chosen to encode the Born rule. Those are the bills the program still has to pay.