SigmaLayer/BornFibrePartition: the record-layer fibre partition (MD-1)

Category: 7-SigmaLayer (the record layer — measurement as a Born partition of the fibre).

The record-layer (MD-1) obligation, discharged on a concrete fibre. For a sharp preparation the epistemic base is pinned (π(ω) = [ψ]) and the measurement carves the ontic fibre into outcome cells; the outcome is the ontic selection of which cell the fibre point occupies, and Born is the fibre measure of the cell. Per the decomposition in specs/record-layer-plan.md §3b–§3c, a measurement factorises as

(moment-map rates) × (a Born partition of the fibre) ,

where the rates rᵢ = |⟨eᵢ|ψ⟩|² = momentMap([ψ])ᵢ come from the torus moment map (Papers A/B, LF4/MomentMap.lean), and the fibre-partition factor produces, from any probability vector r, a partition of the fibre into cells of measure rᵢ. This file discharges the fibre-partition factor on the fibre F = ℝ with Lebesgue measure, via the cumulative (CDF) cells: cdfCell r i is the interval [∑_{j<i} rⱼ, ∑_{j≤i} rⱼ), and volume (cdfCell r i) = rᵢ (volume_cdfCell). The cells are pairwise disjoint (cdfCell_pairwiseDisjoint), so — feeding the Born rates rᵢ = ‖ψ i‖² — the fibre measure of outcome i is exactly the Born weight (volume_bornCell), and the outcome map (fibreOutcome) is the ontic selection ξ ↦ i.

Honest scope: the interval [0,1)+CDF is one concrete Born partition — the point here is the interface + the measure identity, foundational-triple, no sorry. The genuinely open piece is the dynamical realisation (a de-isolation flow / mixing environment whose target-measures are ∝ the moment map — the first-passage picture, record-layer-plan.md §3c); the fibre object it must produce is exactly cdfCell here.

References

specs/record-layer-plan.md (the record layer, MD-1; §3b–§3c the decomposition + dynamics); LF1/Outcomes.lean (OutcomeRegion, the volume-ratio weight); LF4/MomentMap.lean (momentMap_mk_eq_inner_sq, the rates).

noncomputable def CSD.RecordLayer.loSum {n : ℕ} (r : Fin n → ℝ) (i : Fin n) : ℝ

Cumulative sum strictly below i: ∑_{j < i} rⱼ.

Equations

• CSD.RecordLayer.loSum r i = ∑ j : Fin n with ↑j < ↑i, r j

def CSD.RecordLayer.cdfCell {n : ℕ} (r : Fin n → ℝ) (i : Fin n) : Set ℝ

The cumulative (CDF) outcome cell for outcome i: the fibre interval [∑_{j<i} rⱼ, (∑_{j<i} rⱼ) + rᵢ) on F = ℝ. For a probability vector r these partition [0,1).

Equations

• CSD.RecordLayer.cdfCell r i = Set.Ico (CSD.RecordLayer.loSum r i) (CSD.RecordLayer.loSum r i + r i)

theorem CSD.RecordLayer.measurableSet_cdfCell {n : ℕ} (r : Fin n → ℝ) (i : Fin n) : MeasurableSet (cdfCell r i)

theorem CSD.RecordLayer.volume_cdfCell {n : ℕ} (r : Fin n → ℝ) (i : Fin n) : MeasureTheory.volume (cdfCell r i) = ENNReal.ofReal (r i)

The fibre-partition measure identity: the fibre measure of outcome i equals the rate rᵢ. The CDF cell has Lebesgue measure exactly rᵢ. This is the record-layer obligation for the fibre-partition factor; feeding the Born rates gives the Born weight (volume_bornCell).

theorem CSD.RecordLayer.loSum_add_le_loSum {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) {i j : Fin n} (hij : ↑i < ↑j) : loSum r i + r i ≤ loSum r j

The cumulative cell for i ends at or before the cell for j > i begins: (∑_{k<i} rₖ) + rᵢ ≤ ∑_{k<j} rₖ (needs r ≥ 0). This is the ordering that makes the cells a genuine partition of the fibre.

theorem CSD.RecordLayer.cdfCell_disjoint_of_lt {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) {i j : Fin n} (hij : ↑i < ↑j) : Disjoint (cdfCell r i) (cdfCell r j)

The CDF cells of outcomes i < j are disjoint (given r ≥ 0): cell i ends before cell j starts.

theorem CSD.RecordLayer.cdfCell_pairwiseDisjoint {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) : Pairwise (Function.onFun Disjoint (cdfCell r))

The CDF cells are pairwise disjoint (given r ≥ 0): the fibre is genuinely partitioned into outcome cells, so the outcome map is a well-defined ontic selection and the Born weights are additive.

noncomputable def CSD.RecordLayer.fibreOutcome {n : ℕ} (r : Fin n → ℝ) (ξ : ℝ) : Option (Fin n)

The outcome map (the ontic record): the fibre point ξ selects outcome i when it lies in cdfCell r i; none off the cells. For a probability vector this is total off a null set.

Equations

• CSD.RecordLayer.fibreOutcome r ξ = if h : ∃ (i : Fin n), ξ ∈ CSD.RecordLayer.cdfCell r i then some h.choose else none

theorem CSD.RecordLayer.fibreOutcome_eq_some_iff {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) (ξ : ℝ) (i : Fin n) : fibreOutcome r ξ = some i ↔ ξ ∈ cdfCell r i

The ontic selection is the record. For r ≥ 0 (disjoint cells) the outcome map records i at a fibre point exactly when that point lies in the outcome-i cell: fibreOutcome r ξ = some i ↔ ξ ∈ cdfCell r i. So reading the outcome and testing membership in the record event agree.

The Born rates and the record-layer Born identity

noncomputable def CSD.RecordLayer.bornRate {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (i : Fin n) : ℝ

The Born rate of outcome i for state ψ: the squared component magnitude ‖ψ i‖² = |⟨eᵢ, ψ⟩|² (standard/computational-basis context).

Equations

• CSD.RecordLayer.bornRate ψ i = ‖ψ.ofLp i‖ ^ 2

theorem CSD.RecordLayer.bornRate_nonneg {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (i : Fin n) : 0 ≤ bornRate ψ i

theorem CSD.RecordLayer.sum_bornRate {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) : ∑ i : Fin n, bornRate ψ i = ‖ψ‖ ^ 2

The Born rates form a probability vector on a unit state: ∑ᵢ ‖ψ i‖² = ‖ψ‖² = 1.

theorem CSD.RecordLayer.sum_bornRate_unit {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) : ∑ i : Fin n, bornRate ψ i = 1

theorem CSD.RecordLayer.volume_bornCell {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (i : Fin n) : MeasureTheory.volume (cdfCell (bornRate ψ) i) = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)

Record-layer Born identity. The fibre measure of the outcome-i cell, at the Born rates, equals the Born weight ‖ψ i‖² = |⟨eᵢ, ψ⟩|². So measurement outcome frequencies are the fibre volumes of the CDF cells fed by the moment-map rates — the record layer's measure content, foundational-triple, no sorry.

theorem CSD.RecordLayer.volume_iUnion_cdfCell {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) : MeasureTheory.volume (⋃ (i : Fin n), cdfCell r i) = ENNReal.ofReal (∑ i : Fin n, r i)

Additivity. The disjoint CDF cells cover a fibre set of total measure ∑ᵢ rᵢ — the fibre partition is measure-additive across outcomes (via measure_iUnion on the pairwise-disjoint cells).

theorem CSD.RecordLayer.volume_iUnion_bornCell_unit {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) : MeasureTheory.volume (⋃ (i : Fin n), cdfCell (bornRate ψ) i) = 1

The record-layer Born normalisation. For a unit state the Born cells partition a fibre set of measure exactly 1: the total ontic typicality of all outcomes is certainty. The fibre measure of each cell is the Born weight (volume_bornCell), the cells are disjoint (cdfCell_pairwiseDisjoint), and together they carry unit measure — the complete measure content of the record layer's fibre-partition factor, foundational-triple, no sorry.

theorem CSD.RecordLayer.fibreOutcome_eq_none_iff {n : ℕ} (r : Fin n → ℝ) (ξ : ℝ) : fibreOutcome r ξ = none ↔ ∀ (i : Fin n), ξ ∉ cdfCell r i

fibreOutcome is none exactly off every cell — the companion of fibreOutcome_eq_some_iff, and what identifies the leftover set as a complement.