The two preparation interfaces agree: the ρ_ep of Q28 is the density in W3's formula

Category: 7-SigmaLayer (the seam between SigmaLayer.Preparation / ProjectiveSector and LF2.SectorData / fromPreparation; item 4 of the 2026-09-11 QIT follow-ups).

The corpus carries two preparation interfaces. The SigmaLayer core (ConstraintDynamics, Preparation, ProjectiveSector) has region preparations, their conditional Liouville laws, and Q28's theorem that the projective law of a region preparation is μFS.withDensity ρ_ep (projectivePreparationLaw_withDensity). The LF2 interface (SectorData, MeasureBridgeData, fromPreparation) has the density operator of a preparation and, since W3, its entrywise ρ_ep form preparationDensity_apply_rnDeriv, which took absolute continuity of the projective law as a hypothesis. Until 2026-09-11 nothing composed the two. This module does:

• ProjectiveSector.toSectorData, ProjectiveSector.toMeasureBridgeData — the adapter: a projective sector, a region preparation and the group data LF2's SectorData asks for (a measurable Liouville-invariant G-action on Σ, intertwined by the projection with a measurable transitive action on the target, μFS invariant) assemble into an LF2 sector with its bridge;
• ★★ preparationDensity_apply_rhoEp — the seam: for a region preparation with a bridge, the LF2 density operator of its conditional law is ∫ ρ_ep(ψ) ψⱼ conj ψₖ dμFS(ψ) with ρ_ep Q28's Radon–Nikodym density (ProjectiveSector.preparationDensity). The absolute continuity is the theorem projectivePreparationLaw_absolutelyContinuous, no longer a hypothesis;
• ★★ kahler_preparationDensity_apply, kahler_preparationDensity_apply_unitSection — on the Kähler arena the seam closes with no hypotheses: for any dynamics on ℂℙ^{N−1} × T² carrying the Liouville measure and any region preparation, the corpus's kSectorData / kBridgeData (c = 1) density operator is ∫ ρ_ep |ψ⟩⟨ψ| dμ_FS with ρ_ep the density of kahler_preparation_density against the Fubini–Study measure, and with the canonical measurable unit section as representative not even a representative is chosen.

Honest scope

The adapter takes the G-action as data because the SigmaLayer core has none and LF2's SectorData requires one; on the Kähler arena it is the unitary group and already built (kSectorData). The adapter's ontic setup fixes a time t (Preparation.toOnticSetup); the density operator does not depend on it. Nothing here changes the posits: the sector and its Liouville law remain Posits 2 and 3 of specs/POSITS.md.

References: specs/qit-chain-scoping.md; SigmaLayer/PreparationDensity.lean (Q28); LF2/PreparationBarycenter.lean (W3); LF4/KahlerInstance.lean (kSectorData), LF4/KahlerWignerLift.lean (kBridgeData); SigmaLayer/Adapters.lean.

The adapter: a projective sector with group data is an LF2 sector

def CSD.SigmaLayer.ProjectiveSector.toSectorData {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {N : ℕ} {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) (t : OnticTime) {G : Type u_2} [Group G] [MulAction G Sigma] [MulAction G (ProjectiveState N)] [MulAction.IsPretransitive G (ProjectiveState N)] (hσ : ∀ (g : G), Measurable fun (x : Sigma) => g • x) (hP : ∀ (g : G), Measurable fun (x : ProjectiveState N) => g • x) (hinv : ∀ (g : G), MeasureTheory.MeasurePreserving (fun (x : Sigma) => g • x) ↑D.muL ↑D.muL) (hequiv : ∀ (g : G) (x : Sigma), Q.pi (g • x) = g • Q.pi x) : LF2.SectorData Sigma (ProjectiveState N) G

The LF2 adapter. A SigmaLayer projective sector, a region preparation (for the LF1 ontic setup at time t), and the group data LF2's SectorData asks for — a measurable, Liouville- invariant G-action on Σ intertwined by pi with a measurable transitive action on the projective target — assemble into an LF2.SectorData.

Equations

• Q.toSectorData P t hσ hP hinv hequiv = { toOntic := P.toOnticSetup t, π := Q.pi, measurable_π := ⋯, measurable_smul_σ := hσ, measurable_smul_P := hP, hμL_inv := hinv, hπ_equiv := hequiv }

def CSD.SigmaLayer.ProjectiveSector.toMeasureBridgeData {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {N : ℕ} {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) (t : OnticTime) {G : Type u_2} [Group G] [MulAction G Sigma] [MulAction G (ProjectiveState N)] [MulAction.IsPretransitive G (ProjectiveState N)] (hσ : ∀ (g : G), Measurable fun (x : Sigma) => g • x) (hP : ∀ (g : G), Measurable fun (x : ProjectiveState N) => g • x) (hinv : ∀ (g : G), MeasureTheory.MeasurePreserving (fun (x : Sigma) => g • x) ↑D.muL ↑D.muL) (hequiv : ∀ (g : G) (x : Sigma), Q.pi (g • x) = g • Q.pi x) (μFS : MeasureTheory.Measure (ProjectiveState N)) (c : ENNReal) (hbridge : Q.projectiveLaw ↑D.muL = c • μFS) (hFS_inv : ∀ (g : G), MeasureTheory.MeasurePreserving (fun (x : ProjectiveState N) => g • x) μFS μFS) : LF2.MeasureBridgeData (Q.toSectorData P t hσ hP hinv hequiv) μFS

The adapter's measure bridge: the SigmaLayer bridge pi_* muL = c • μFS and G-invariance of μFS are LF2's MeasureBridgeData.

Equations

• Q.toMeasureBridgeData P t hσ hP hinv hequiv μFS c hbridge hFS_inv = { is_inv := hFS_inv, c := c, bridge_eq := hbridge }

The seam: the ρ_ep of Q28 is the density in W3's formula

theorem CSD.SigmaLayer.preparationDensity_apply_rhoEp {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {N : ℕ} {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) (t : OnticTime) {G : Type u_2} [Group G] [MulAction G Sigma] [MulAction G (ProjectiveState N)] [MulAction.IsPretransitive G (ProjectiveState N)] (hσ : ∀ (g : G), Measurable fun (x : Sigma) => g • x) (hP : ∀ (g : G), Measurable fun (x : ProjectiveState N) => g • x) (hinv : ∀ (g : G), MeasureTheory.MeasurePreserving (fun (x : Sigma) => g • x) ↑D.muL ↑D.muL) (hequiv : ∀ (g : G) (x : Sigma), Q.pi (g • x) = g • Q.pi x) (μFS : MeasureTheory.Measure (ProjectiveState N)) [MeasureTheory.IsProbabilityMeasure μFS] (c : ENNReal) (hbridge : Q.projectiveLaw ↑D.muL = c • μFS) (hFS_inv : ∀ (g : G), MeasureTheory.MeasurePreserving (fun (x : ProjectiveState N) => g • x) μFS μFS) (rep : ProjectiveState N → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : ProjectiveState N), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (j k : Fin N) : (LF2.preparationDensity (Q.toSectorData P t hσ hP hinv hequiv) μFS (Q.toMeasureBridgeData P t hσ hP hinv hequiv μFS c hbridge hFS_inv) (↑P.conditionalMeasure) rep hrep_unit hrep_meas).M j k = ∫ (ψ : ProjectiveState N), (Q.preparationDensity P μFS ψ).toReal • ((rep ψ).ofLp j * star ((rep ψ).ofLp k)) ∂μFS

★★ The two preparation interfaces agree on the density operator. For a region preparation P of the SigmaLayer with a bridge pi_* muL = c • μFS, the LF2 density operator of its conditional law (W3's barycentre) is, entrywise, ∫ ρ_ep(ψ) ψⱼ conj ψₖ dμFS(ψ) with ρ_ep the Radon–Nikodym density of Q28 (ProjectiveSector.preparationDensity). The absolute continuity W3's ρ_ep form took as a hypothesis is here the theorem projectivePreparationLaw_absolutelyContinuous.

The Kähler arena: the seam at c = 1

theorem CSD.SigmaLayer.kahler_preparationDensity_apply {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] (D : ConstraintDynamics (LF4.KSigma N)) (hmuL : ↑D.muL = LF4.kMuL p₀) (P : Preparation D) (rep : LF4.CPN N → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : LF4.CPN N), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (j k : Fin N) : (LF2.preparationDensity (LF4.kSectorData p₀) (Matrix.UnitaryGroup.fsMeasure p₀) (LF4.kBridgeData p₀) (↑P.conditionalMeasure) rep hrep_unit hrep_meas).M j k = ∫ (ψ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), ((kahlerFstSector D).preparationDensity P (Matrix.UnitaryGroup.fsMeasure p₀) ψ).toReal • ((rep ψ).ofLp j * star ((rep ψ).ofLp k)) ∂Matrix.UnitaryGroup.fsMeasure p₀

★★ On the Kähler arena the seam closes with no hypotheses. For any dynamics on Σ = ℂℙ^{N−1} × T² carrying the Liouville measure and any region preparation P, the LF2 density operator of P (with respect to the corpus's kSectorData and its axiom-free bridge kBridgeData, c = 1) is ∫ ρ_ep(ψ) |ψ⟩⟨ψ| dμ_FS(ψ) entrywise, with ρ_ep the Q28 density of kahler_preparation_density against THE Fubini–Study measure.

theorem CSD.SigmaLayer.kahler_preparationDensity_apply_unitSection {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] (D : ConstraintDynamics (LF4.KSigma N)) (hmuL : ↑D.muL = LF4.kMuL p₀) (P : Preparation D) (j k : Fin N) : (LF2.preparationDensity (LF4.kSectorData p₀) (Matrix.UnitaryGroup.fsMeasure p₀) (LF4.kBridgeData p₀) (↑P.conditionalMeasure) Projectivization.unitSection ⋯ ⋯).M j k = ∫ (ψ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), ((kahlerFstSector D).preparationDensity P (Matrix.UnitaryGroup.fsMeasure p₀) ψ).toReal • (ψ.unitSection.ofLp j * star (ψ.unitSection.ofLp k)) ∂Matrix.UnitaryGroup.fsMeasure p₀

The Kähler seam with the canonical measurable unit section as representative: no representative hypothesis either.