SigmaLayer/MeasureBridge: the projective measure bridge and its concrete product proof

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

Bridge assumption B1: the ontic measure pushes forward under pi to the required projective measure. This is an explicit assumption interface in the abstract theory (ProjectiveMeasureBridge, HasFubiniStudyPushforward), and a THEOREM for concrete models. Here the concrete model is the many-to-one product sector Sigma = CP^{N-1} x T^2, pi = Prod.fst, muL = muFS ⊗ vol, adapted to the SigmaLayer core from manyToOneSchrodingerSetup; the pushforward pi_* muL = muFS is discharged by the existing manyToOneSetup_baseVolume_eq_fubiniStudy (which reuses Measure.fst_prod).

We do NOT install the Fubini-Study equality as a typeclass instance for every projective sector; it is a named field / predicate, proved only where a concrete model supplies it.

Consistency witness, not derivation. On the concrete product model the Liouville measure is muL = muFS ⊗ vol — the Fubini-Study measure is built IN — so pi_* muL = muFS is a compatibility fact about the witness (Measure.fst_prod on a product whose first factor already IS muFS), NOT a derivation of the Fubini-Study measure from a more primitive ontology. That muFS is the sector's typicality law is the SO-1 posit — it reduces to D1, the dynamical sector origin (⚠️ RESIDUE(R-012)); "derive the sector" itself is a retired framing (specs/reconstruction-status.md §7).

structure CSD.SigmaLayer.ProjectiveMeasureBridge {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) : Type

Projective measure bridge (B1 interface). A named assumption that pi_* muL equals a specified target projective measure. Passive data, not a typeclass.

• targetMeasure : MeasureTheory.Measure (ProjectiveState N)

  The target projective measure.

• map_muL : MeasureTheory.Measure.map Q.pi ↑D.muL = self.targetMeasure

  The pushforward of the Liouville measure under pi equals the target.

def CSD.SigmaLayer.HasFubiniStudyPushforward {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (p₀ : ProjectiveState N) : Prop

The Fubini-Study pushforward predicate (B1 with a fixed target). pi_* muL = muFS. A theorem target for concrete models, not a global instance.

Equations

• CSD.SigmaLayer.HasFubiniStudyPushforward Q p₀ = (MeasureTheory.Measure.map Q.pi ↑D.muL = Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The concrete many-to-one product instance (B1 proved)

noncomputable def CSD.SigmaLayer.productDynamics {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : ConstraintDynamics (LF4.KSigma (M + 1))

The many-to-one product sector as an SigmaLayer ConstraintDynamics, adapted from manyToOneSchrodingerSetup (unitary flow exp(-itH) on the base ray, fibre fixed). The one-parameter group laws come from expNegITH_unitary_group.

Equations

• CSD.SigmaLayer.productDynamics H hH p₀ = CSD.SigmaLayer.kahlerConstraintDynamics (CSD.LF4.manyToOneSchrodingerSetup H hH p₀) ⋯ ⋯

noncomputable def CSD.SigmaLayer.productSector {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : ProjectiveSector (M + 1) (productDynamics H hH p₀)

The many-to-one product projective sector: pi = Prod.fst onto the ray space.

Equations

• CSD.SigmaLayer.productSector H hH p₀ = CSD.SigmaLayer.kahlerProjectiveSector (CSD.LF4.manyToOneSchrodingerSetup H hH p₀)

theorem CSD.SigmaLayer.productSector_hasFubiniStudyPushforward {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : HasFubiniStudyPushforward (productSector H hH p₀) p₀

B1 proved for the product model. The projective law of the product Liouville measure is the Fubini-Study measure: pi_* (muFS ⊗ vol) = muFS. Discharged by manyToOneSetup_baseVolume_eq_fubiniStudy. This is the concrete instance of the measure bridge, not an assumption.

noncomputable def CSD.SigmaLayer.productMeasureBridge {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : ProjectiveMeasureBridge (productSector H hH p₀)

The product measure bridge as a bundled ProjectiveMeasureBridge with target muFS.

Equations

• CSD.SigmaLayer.productMeasureBridge H hH p₀ = { targetMeasure := Matrix.UnitaryGroup.fubiniStudyMeasure p₀, map_muL := ⋯ }