LF2 Measure Bridge

Category: 3-Local (LF2 π_* μL = c · μFS bridge ingredients).

Three pieces (spec §3.3, Lemma 1, Lemma 2):

1. pushforward_apply — thin wrapper over Measure.map_apply specialised to a SectorData's projection.
2. preimage_action_eq — the preimage/action identity π⁻¹((g • ·) '' A) = (g • ·) '' (π⁻¹(A)) (the MulAction form; the earlier epAction/onticAction named maps were removed in the MulAction migration).
3. pushforward_epAction_invariant — the pushforward π*μL is invariant under the induced G-action on P.

The measure bridge π*μL = c • μFS (spec Theorem 1) follows from (3) plus uniqueness of the G-invariant measure. On the concrete instances the bridge holds axiom-free (CSD.LF4.cp_measure_bridge, k_measure_bridge — c = 1, trivial / product-marginal fibres). The earlier abstract over-general statement measure_bridge and the imported invariant_measure_uniqueness axiom it required were removed (2026-06-04): nothing downstream used the abstract version, and the concrete CP^{N-1} uniqueness it would have needed is itself a proved, axiom-free theorem in the tree (Matrix.UnitaryGroup.invariant_measure_uniqueness_cpn). The last remaining imported axiom, busch_effect_gleason, was itself discharged 2026-07-21 (proved as effect_gleason_representation); the corpus now imports zero axioms.

theorem CSD.LF2.SectorData.pushforward_apply {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) {A : Set P} (hA : MeasurableSet A) : (MeasureTheory.Measure.map D.π D.μL) A = D.μL (D.π ⁻¹' A)

Pushforward rewrite for the projection, specialised form of Measure.map_apply.

theorem CSD.LF2.SectorData.preimage_action_eq {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) (g : G) (A : Set P) : D.π ⁻¹' (fun (x : P) => g • x) '' A = (fun (x : SigmaSpace) => g • x) '' D.π ⁻¹' A

Lemma 1 of the spec. Preimage/action identity: pulling back an epistemic orbit along π equals pushing the preimage through the ontic action. Consequence of π-equivariance + bijectivity of the action.

theorem CSD.LF2.SectorData.pushforward_epAction_invariant {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) (g : G) : MeasureTheory.MeasurePreserving (fun (x : P) => g • x) (MeasureTheory.Measure.map D.π D.μL) (MeasureTheory.Measure.map D.π D.μL)

Lemma 2 of the spec. The pushforward measure π*μL is invariant under the induced G-action on P.