SigmaLayer/OutcomeBasin: basins for a K-outcome field

Category: 7-SigmaLayer (the record layer — generalisation bridge).

OutcomeField.lean decoupled the outcome count from the dimension but left the bridge unbuilt: globalBasin still consumed a ContextField, so a K-outcome field could not drive the record layer. This file builds that bridge, so degenerate projective measurements reach the basins.

The construction is the same one — the rate field is read at the ontic point, and the basin is the CDF arc it determines — with Fin K in place of Fin N.

What is proved

• outcomeBasin — Bᵢ(c) = {x | x.2.1 ∈ circleCell (c.rate x.1) i} for c : OutcomeField N K.
• measurableSet_outcomeBasin, outcomeBasin_pairwiseDisjoint.
• outcomeBasin_prob — conditioning on p returns rate p i.
• outcomeBasin_ae_total.
• outcomeBasin_toOutcomeField — ★ conservativity: for a ContextField this is definitionally globalBasin. The generalisation adds cases without changing any existing one.

⚠️ Scope

Still kinematic, and δ_p ⊗ Haar is still the epistemic measure taken as a definition rather than a disintegration — inherited unchanged from GlobalBasin.lean. Driving the dynamical layer with a K-outcome field additionally needs the shear witness's index function generalised, which is not done here.

References

SigmaLayer/OutcomeField.lean (OutcomeField, blockField); SigmaLayer/GlobalBasin.lean (the K = N original this generalises).

theorem CSD.RecordLayer.OutcomeField.loSum_le_one {N K : ℕ} (c : OutcomeField N K) (p : LF4.CPN N) (i : Fin K) : loSum (c.rate p) i + c.rate p i ≤ 1

theorem CSD.RecordLayer.OutcomeField.measurable_loSum {N K : ℕ} (c : OutcomeField N K) (i : Fin K) : Measurable fun (p : LF4.CPN N) => loSum (c.rate p) i

noncomputable def CSD.RecordLayer.outcomeBasin {N K : ℕ} (c : OutcomeField N K) (i : Fin K) : Set (LF4.KSigma N)

The basin of outcome i for a K-outcome field.

Equations

• CSD.RecordLayer.outcomeBasin c i = {x : CSD.LF4.KSigma N | x.2.1 ∈ CSD.RecordLayer.circleCell (c.rate x.1) i}

theorem CSD.RecordLayer.outcomeBasin_toOutcomeField {N : ℕ} (c : ContextField N) (i : Fin N) : outcomeBasin c.toOutcomeField i = globalBasin c i

★ Conservativity: for a ContextField the generalised basin is globalBasin, definitionally.

theorem CSD.RecordLayer.measurableSet_outcomeBasin {N K : ℕ} (c : OutcomeField N K) (i : Fin K) : MeasurableSet (outcomeBasin c i)

theorem CSD.RecordLayer.outcomeBasin_pairwiseDisjoint {N K : ℕ} (c : OutcomeField N K) : Pairwise (Function.onFun Disjoint (outcomeBasin c))

theorem CSD.RecordLayer.preimage_outcomeBasin {N K : ℕ} (c : OutcomeField N K) (i : Fin K) (p : LF4.CPN N) : Prod.mk p ⁻¹' outcomeBasin c i = torusCell (c.rate p) i

theorem CSD.RecordLayer.outcomeBasin_prob {N K : ℕ} (c : OutcomeField N K) (i : Fin K) (p : LF4.CPN N) : (epistemicMeasure p) (outcomeBasin c i) = ENNReal.ofReal (c.rate p i)

Conditioning on the preparation returns the rate, for any number of outcomes.

theorem CSD.RecordLayer.outcomeBasin_ae_total {N K : ℕ} (c : OutcomeField N K) (p : LF4.CPN N) : (epistemicMeasure p) (Set.univ \ ⋃ (i : Fin K), outcomeBasin c i) = 0