SigmaLayer/FibredSigma: the fibred ontic space Σ = base × fibre (MD-1)

Category: 7-SigmaLayer (the record layer — the base×fibre ontic space).

Assembles the honest CSD ontic space as a product Σ = base × fibre = CPN n × ℝ, realising the epistemic/ontic split of Papers C/D directly in the geometry:

• the base CPN n = ℂℙⁿ⁻¹ carries the epistemic projective point — for a sharp preparation ψ it is pinned to [ψ] (baseProj_sharpTypicality), matching Paper C's epistemic outcome regions Ωᵢ(M) living on projective space;
• the fibre ℝ carries the ontic record coordinate — the measurement carves the fibre into the Born partition (cdfCell), and the outcome is the fibre point's basin;
• the projection baseProj = π : Σ → base recovers the epistemic point from the ontic state.

For a sharp preparation the typicality measure is sharpTypicality = δ_{[ψ]} ⊗ fibreTypicality — the base pinned (Dirac), the fibre uniform — so the ontic support is {[ψ]} × [0,1). The Born weight of an outcome is then the product-measure typicality of its fibre event, which is exactly the fibre measure (sharpTypicality_fibredEvent): ‖ψ i‖², the Kähler moment map (sharpTypicality_fibredEvent_momentMap).

So this ties SigmaLayer/FibreRecord.lean (the fibre) to the projective base: the ψ-dependence sits in the base (the epistemic point / the preparation), the fibre carries the context-fixed outcome partition, and Born is the ontic typicality of the fibre event over the pinned base — the epistemic (base) / ontic (fibre) split made literal. Foundational-triple, no sorry.

References

specs/record-layer-plan.md (record layer, MD-1; epistemic base / ontic fibre); SigmaLayer/FibreRecord.lean (the fibre partition + record); SigmaLayer/MomentMapRace.lean (bornRate_eq_momentMap); Paper C A7 (epistemic Ωᵢ(M) ⊂ ℂℙⁿ⁻¹), Paper D (ontic/epistemic split).

@[reducible, inline]

abbrev CSD.RecordLayer.FibredSigma (n : ℕ) : Type

The fibred ontic space Σ = base × fibre = CPN n × ℝ: the base is the epistemic projective point, the fibre the ontic record coordinate.

Equations

• CSD.RecordLayer.FibredSigma n = (CSD.LF4.CPN n × ℝ)

def CSD.RecordLayer.baseProj {n : ℕ} : FibredSigma n → LF4.CPN n

The projection to the epistemic base π : Σ → CPN n.

Equations

• CSD.RecordLayer.baseProj = Prod.fst

noncomputable def CSD.RecordLayer.sharpTypicality {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ0 : ψ ≠ 0) : MeasureTheory.Measure (FibredSigma n)

The sharp-preparation typicality measure: δ_{[ψ]} ⊗ fibreTypicality — the base pinned at the epistemic point [ψ], the fibre uniform on [0,1). Ontic support {[ψ]} × [0,1).

Equations

• CSD.RecordLayer.sharpTypicality ψ hψ0 = (MeasureTheory.Measure.dirac (Projectivization.mk ℂ ψ hψ0)).prod CSD.RecordLayer.fibreTypicality

instance CSD.RecordLayer.instIsProbabilityMeasureFibredSigmaSharpTypicality {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ0 : ψ ≠ 0) : MeasureTheory.IsProbabilityMeasure (sharpTypicality ψ hψ0)

def CSD.RecordLayer.fibredEvent {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (i : Fin n) : Set (FibredSigma n)

The fibre event of outcome i: the ontic states whose fibre coordinate lies in the Born partition cell i (any base). The outcome depends only on the fibre.

Equations

• CSD.RecordLayer.fibredEvent ψ i = Set.univ ×ˢ CSD.RecordLayer.cdfCell (CSD.RecordLayer.bornRate ψ) i

theorem CSD.RecordLayer.mem_fibredEvent_iff {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (i : Fin n) (ω : FibredSigma n) : ω ∈ fibredEvent ψ i ↔ ω.2 ∈ cdfCell (bornRate ψ) i

theorem CSD.RecordLayer.baseProj_sharpTypicality {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ0 : ψ ≠ 0) : MeasureTheory.Measure.map baseProj (sharpTypicality ψ hψ0) = MeasureTheory.Measure.dirac (Projectivization.mk ℂ ψ hψ0)

The base is pinned to the epistemic point. For a sharp preparation the projection π sends the typicality measure to the Dirac at [ψ]: the base coordinate is epistemically fixed at [ψ].

theorem CSD.RecordLayer.sharpTypicality_fibredEvent {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin n) : (sharpTypicality ψ hψ0) (fibredEvent ψ i) = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)

Born = the ontic typicality of the fibre event on the assembled Σ. For a unit state the sharpTypicality measure of the outcome-i fibre event is exactly ‖ψ i‖² — the base being pinned (Dirac, mass 1) contributes nothing, so the Born weight is the fibre typicality of the cell.

theorem CSD.RecordLayer.sharpTypicality_fibredEvent_momentMap {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin n) : (sharpTypicality ψ hψ0) (fibredEvent ψ i) = ENNReal.ofReal (LF4.momentMap (Projectivization.mk ℂ ψ hψ0) i)

The Born weight of the fibre event is the Kähler moment-map coordinate at [ψ].