Epistemic measure

Condition on what a preparation actually fixes and the leftover ignorance is a measure -- and it is now a theorem, not a stipulation: the arena's own volume disintegrates into exactly this.

proved in corpus · proved here, no imported axiomsLean epistemicMeasure_eq_disintegration

In plain terms

Here is the problem. You prepared the system carefully, so you know its quantum state exactly. On the arena picture that knowledge is radically incomplete: one state corresponds to a whole crowd of microstates, all projecting to the same point. What should you believe about the part you cannot see?

The natural answer: you know the visible coordinate exactly, so put all your credence there; you know nothing about the hidden coordinate, so spread your credence evenly over it, using the fibre's own symmetry to define "evenly". That combined object is the epistemic measure.

The satisfying part is that "evenly" is not a choice. The arena's own volume, disintegrated along the projection -- sliced into per-state fibres -- gives exactly this measure, almost everywhere. What began as a stated definition was later proved to be the unique answer the geometry had waiting.

In CSD

The epistemic measure is what "isolation is conditioning" means in practice: the isolation-conditioned state of knowledge at preparation p is the Dirac mass at p on the base times normalised Haar on the fibre. Every record-layer probability -- including the Born weights of the context-fixed basins -- is computed against it.

Because conditioning on a single state conditions on a set the base measure calls null, the corpus originally took the Dirac-times-Haar form as a stated definition. The derivation has since landed: the Liouville measure disintegrates along the base projection, its disintegration kernel is almost everywhere the constant Haar kernel, and the epistemic measure is the fibre of that disintegration planted at its base point. The modelling choice turned out to be the theorem.

Mathematically

epistemicMeasure p is the product of the Dirac measure at p with normalised Haar on the torus fibre -- a probability measure on the arena for every p. The derivation: kMuL_condKernel_ae identifies the disintegration kernel of the Liouville measure with the constant Haar kernel, almost everywhere in the Fubini-Study base measure, via the standard-Borel conditional-kernel machinery and almost-everywhere uniqueness of disintegrations; epistemicMeasure_eq_disintegration then equates the epistemic measure with the Dirac-paired disintegration fibre. The almost-everywhere qualifier is intrinsic: disintegration kernels are only determined up to a null set of base points.

Module
CsdLean4/RecordLayer/EpistemicDisintegration.lean
Related
liouville measure, haar measure, outcome region, typicality, ontic vs epistemic

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy