SigmaLayer/DeIsolationFlow: the de-isolation outcome distribution (MD-1, step 2b′)

Category: 7-SigmaLayer (the record layer — the de-isolation flow's outcome distribution).

This is the outcome-distribution layer of the record layer (MD-1), built on the fibre partition of BornFibrePartition.lean. Where that file gives the per-cell fibre measures, this file gives the outcome distribution carried by the canonical fibre typicality measure fibreTypicality (Lebesgue measure restricted to the unit fibre [0,1), a probability measure), and the abstract de-isolation flow ⟹ Born bridge.

The picture (plan specs/record-layer-plan.md §3c): a measurement is a de-isolation flow Φ_M on the fibred Σ; its pointer p = readout ∘ Φ_M : F → Fin n sends a fibre point to the outcome whose basin it lands in, and Born is the fibre-typicality volume of the basin — a typicality volume of a flow-carved basin, not injected noise.

What is proved here, foundational-triple, no sorry:

• fibreTypicality is a probability measure (instIsProbabilityMeasure, fibreTypicality_Ico01).
• Outcome probability = Born weight: for a unit state the fibre typicality of the Born cell i is exactly ‖ψ i‖² (fibreTypicality_bornCell) — the outcome probability of i.
• The pointer is a.e. defined: the Born cells cover the fibre up to a null set (fibreTypicality_uncovered) — the outcome is determined fibreTypicality-almost everywhere.
• De-isolation flow ⟹ Born (map_pointer_apply): any measurable pointer p whose basins carry the Born cell measures pushes fibreTypicality forward to the Born distribution — outcome i has probability ‖ψ i‖². This is the flow-independent content.

The open research obligation (the wall, plan §3c / staging step 2b′): exhibit a pointer p generated by a physical de-isolation Hamiltonian H_int(M) — p = readout ∘ (flow of H_int(M)) — whose basins are cdfCell (moment map). This file proves the Born conclusion from the basin measures; it does not derive the basins from a Hamiltonian. map_pointer_apply makes the remaining obligation precise: supply a measurable p with fibreTypicality (p⁻¹{i}) = ‖ψ i‖².

Status 2026-08-27 (RecordLayer/ShearDeIsolation.lean): the readout∘flow shape is exhibited — shearDeIsolationInteraction's pointer is the constructed shear propagator's readout (cellPointer_outcomeSector_eq_readout, pointwise) and its basin_rate is discharged from shear_sector_born, on the fibred arena Σ_sel × T²_R with the ontic ready preparation readyPrep [ψ] (not on this file's [0,1) fibre — per the 2026-08-26 scoping the cell shapes are bookkeeping; the fibre, rates and selection are what is carried). The surviving residue is ShearWitness item 1: the propagator's Hamiltonian generation is stated, not formalised (the permanently-scoped symplectic row).

References

specs/record-layer-plan.md §3c (the de-isolation flow / first-passage race; step 2b′); SigmaLayer/BornFibrePartition.lean (the fibre partition — cdfCell, bornRate, volume_bornCell, volume_iUnion_bornCell_unit); LF4/MomentMap.lean (momentMap_mk_eq_inner_sq, the rates).

noncomputable def CSD.RecordLayer.fibreTypicality : MeasureTheory.Measure ℝ

The fibre typicality measure: Lebesgue measure restricted to the unit fibre [0,1). This is the canonical typicality measure the de-isolation flow acts on; the outcome probabilities are the fibre-typicality volumes of the basins.

Equations

• CSD.RecordLayer.fibreTypicality = MeasureTheory.volume.restrict (Set.Ico 0 1)

theorem CSD.RecordLayer.fibreTypicality_Ico01 : fibreTypicality (Set.Ico 0 1) = 1

instance CSD.RecordLayer.instIsProbabilityMeasure : MeasureTheory.IsProbabilityMeasure fibreTypicality

theorem CSD.RecordLayer.cdfCell_subset_Ico {n : ℕ} (r : Fin n → ℝ) (hr : ∀ (i : Fin n), 0 ≤ r i) (i : Fin n) : cdfCell r i ⊆ Set.Ico 0 (∑ j : Fin n, r j)

The CDF cell for outcome i sits inside [0, ∑ⱼ rⱼ) (given r ≥ 0): the cumulative offset is nonnegative and the cell ends at a partial sum ≤ the total.

theorem CSD.RecordLayer.bornCell_subset_Ico01 {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (i : Fin n) : cdfCell (bornRate ψ) i ⊆ Set.Ico 0 1

For a unit state the Born cells lie inside the unit fibre [0,1).

theorem CSD.RecordLayer.iUnion_bornCell_subset_Ico01 {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) : ⋃ (i : Fin n), cdfCell (bornRate ψ) i ⊆ Set.Ico 0 1

theorem CSD.RecordLayer.fibreTypicality_bornCell {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) (i : Fin n) : fibreTypicality (cdfCell (bornRate ψ) i) = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)

Outcome probability = Born weight. For a unit state the fibre typicality of the Born cell i is exactly ‖ψ i‖² = |⟨eᵢ, ψ⟩|² — the de-isolation outcome i occurs with the Born probability.

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

The Born cells cover the unit fibre up to fibre-typicality 1.

theorem CSD.RecordLayer.fibreTypicality_uncovered {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) : fibreTypicality (Set.Ico 0 1 \ ⋃ (i : Fin n), cdfCell (bornRate ψ) i) = 0

The de-isolation pointer is defined almost everywhere. For a unit state the Born cells cover the fibre [0,1) up to a fibreTypicality-null set: the outcome is determined a.e., there is no positive-typicality set on which no outcome is recorded.

theorem CSD.RecordLayer.fibreTypicality_uncovered_univ {n : ℕ} (ψ : EuclideanSpace ℂ (Fin n)) (hψ : ‖ψ‖ = 1) : fibreTypicality (Set.univ \ ⋃ (i : Fin n), cdfCell (bornRate ψ) i) = 0

The [0,1) in fibreTypicality_uncovered is not forced: the same statement holds on univ.

This corrects a reason that several record-layer modules gave for the restriction — that "Lebesgue measure on the line is infinite". fibreTypicality is not Lebesgue measure on the line: it is volume.restrict (Ico 0 1), a probability measure (instIsProbabilityMeasure, proved directly above), so nothing about infinite mass obstructs the univ form.

⚠️ But this theorem is weaker than it looks, and that is the real difference from the compact fibre. It holds because fibreTypicality assigns measure zero to everything outside [0,1) (fibreTypicality_Ici_one): points off the unit fibre are excused by the measure, not covered by cells. On CircleFibre the total mass one is Haar mass on a compact group rather than a restriction imposed by hand, so there is nowhere for an uncovered point to hide. See RecordLayer.circleBornMeasurement_ae_total.

theorem CSD.RecordLayer.fibreTypicality_Ici_one : fibreTypicality (Set.Ici 1) = 0

Why the univ form above is cheap on ℝ. The unit fibre's complement carries infinite Lebesgue measure but zero typicality: fibreTypicality excuses it by fiat. This is the honest statement of what compactifying the fibre buys, and it is a fact about the restriction, not about Lebesgue measure being infinite.

theorem CSD.RecordLayer.map_pointer_apply {n : ℕ} {F : Type u_1} [MeasurableSpace F] {ν : MeasureTheory.Measure F} {p : F → Fin n} (hp : Measurable p) (ψ : EuclideanSpace ℂ (Fin n)) (i : Fin n) (hbasin : ν (p ⁻¹' {i}) = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)) : (MeasureTheory.Measure.map p ν) {i} = ENNReal.ofReal (‖ψ.ofLp i‖ ^ 2)

De-isolation flow ⟹ Born. Any measurable pointer p on the fibre whose basin p⁻¹{i} has the Born cell measure pushes the fibre typicality forward to the Born distribution: the outcome-i mass of fibreTypicality.map p is exactly ‖ψ i‖² = |⟨eᵢ, ψ⟩|².

This is the flow-independent content of step 2b′: given a de-isolation flow whose basins are the moment-map/Born cells, the outcome distribution is Born. The open research obligation (plan §3c) is to exhibit such a p generated by a physical de-isolation Hamiltonian H_int(M); that derivation is not part of this theorem, whose hypothesis hbasin is exactly the obligation.