SigmaLayer/DynamicBorn: the shear witness driven by the context-fixed basins (item 4)

Category: 7-SigmaLayer (the record layer — the dynamical Born rule).

ShearWitness proves the correlation for an abstract measurable index ι. This file supplies the index the architecture actually intends — the one read off the context-fixed basins — so that the dynamical outcome sectors carry the Born weights.

What is proved

• basinIndex — the outcome index read off globalBasin, and measurable_basinIndex. The fibre over i is globalBasin c i, except over the default index where it also picks up the (null) set of points in no basin at all.
• measure_basinIndex_fibre — that null set costs nothing: the fibre has exactly the basin's measure.
• shear_selector_born — the selector-and-ready sectors carry the Born weights.

⚠️ Scope

Unchanged from ShearWitness: the propagator is explicit and every property is proved of it, but the Hamiltonian generation is stated, not formalised (Mathlib has no manifold Hamiltonian-flow API). This file closes the Born half of item 4, not item 3.

References

SigmaLayer/ShearWitness.lean; SigmaLayer/GlobalBasin.lean (globalBasin, globalBasin_born, globalBasin_ae_total); SigmaLayer/MeasurementProtocol.lean (measure_outcomeSector_eq_of_correlates).

The index read off the basins

noncomputable def CSD.RecordLayer.basinIndex {N : ℕ} [NeZero N] (c : ContextField N) (x : LF4.KSigma N) : Fin N

The outcome index of a point of Σ_sel, read off the context-fixed basins. Points in no basin — a null set — are sent to the default index.

Equations

• CSD.RecordLayer.basinIndex c x = if h : ∃ (i : Fin N), x ∈ CSD.RecordLayer.globalBasin c i then h.choose else 0

theorem CSD.RecordLayer.basinIndex_eq_of_mem {N : ℕ} [NeZero N] {c : ContextField N} {x : LF4.KSigma N} {i : Fin N} (hx : x ∈ globalBasin c i) : basinIndex c x = i

theorem CSD.RecordLayer.measurable_basinIndex {N : ℕ} [NeZero N] (c : ContextField N) : Measurable (basinIndex c)

theorem CSD.RecordLayer.measure_basinIndex_fibre {N : ℕ} [NeZero N] (c : ContextField N) (p : LF4.CPN N) (i : Fin N) : (epistemicMeasure p) (basinIndex c ⁻¹' {i}) = (epistemicMeasure p) (globalBasin c i)

The default index's extra fibre costs nothing. The points in no basin form a null set (globalBasin_ae_total), so every fibre of basinIndex carries exactly its basin's measure.

theorem CSD.RecordLayer.shear_selector_born {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) : (epistemicMeasure (Projectivization.mk ℂ ψ hψ0)) (basinIndex (momentContext N) ⁻¹' {i}) = ENNReal.ofReal (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2)

★ The selector-and-ready sectors carry the Born weights.

At preparation ψ, the sector "the hidden selector reads i and the apparatus is ready" has measure ‖⟨eᵢ,ψ⟩‖² under the initial product measure. Composed with shear_correlates and measure_outcomeSector_eq_of_correlates, this is what makes the dynamical outcome weight the Born weight — the probability is transported by the interaction, not posited for it.