Outcome region

An outcome is a region, and the apparatus alone draws its boundary. The preparation decides where the trajectory lands; it does not get to draw the map.

proved in corpus · proved here, no imported axiomsLean globalBasin_born

In plain terms

Here is the problem. If outcome probabilities are sizes of regions, who draws the regions? There is a wrong answer available, and early versions of any volume picture flirt with it: let the prepared state draw its own regions, sized to the probabilities you already knew. That is bookkeeping wearing the costume of an explanation.

The honest requirement is that the measuring device fixes the partition before the state shows up -- the way a roulette wheel's pockets exist before the ball drops. Same wheel for every ball. Then the fact that the frequencies match the pocket sizes is a discovery about the dynamics, not a definition.

CSD's outcome regions meet that requirement: they are built from the apparatus's own data, and no preparation appears anywhere in their definition.

In CSD

The outcome regions are the epistemic half of the two-level structure: a measurement context M fixes a partition of the sector, and Paper C's A7 demands the partition depend on M alone. The corpus discharges this with basins built from a context's rate field read at the ontic point -- the preparation plays no part -- and proves their epistemic weights are exactly the Born weights.

The dimension story is a genuine discovery: at the qubit the regions can live on

the base of the sector, and at higher dimension the natural way of doing so is

squeezed very hard: covariance plus positivity force a chain of machine-checked

conditions on any radial, preparation-only base density -- disjoint supports, and

vanishing below a threshold that rises with dimension -- with the qubit exempted for

the same structural reason three independent ways. Note the scope, because it is

easy to overstate and has been overstated on this page before: that is a tight

constraint, not a no-go. The closing step needs machinery that does not exist yet,

so base-only at higher dimension is open in BOTH directions -- not proved

impossible, not exhibited -- and parked as such. The fibre is where the corpus

builds, by a judgement that either answer would leave unchanged. The regions stay

epistemic throughout; what the trajectory selects among them, the record, is ontic.

Mathematically

A ContextField assigns each base point a measurable probability vector over outcomes; the basin for outcome i is the set of arena points whose fibre coordinate falls in the i-th arc of the field's cumulative weights. Basins are measurable, pairwise disjoint, almost-everywhere exhaustive, and their epistemic probability at preparation psi is the Born weight -- the headline globalBasin_born, from a partition that never mentions psi.

Module
CsdLean4/RecordLayer/GlobalBasin.lean
Related
record layer, epistemic measure, born weight, contextuality, fibre

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