Q28 items 3 and 4b: the projective preparation density ρ_ep, and overlapping preparations

Category: 7-SigmaLayer (BACKLOG Q28, specs/c2-support-plan.md items 3 and 4).

This module is deliberately the FIRST file that speaks both preparation interfaces at once — SigmaLayer.Preparation (region preparations and their conditional measures) and the projective measure bridge (the pushforward of the Liouville measure being a multiple of the Fubini–Study measure). C2 v1.01 tore exactly at that unspoken seam; this module is the seam, spoken.

• Preparation.conditionalMeasure_absolutelyContinuous — the conditional law of a region preparation is absolutely continuous w.r.t. the Liouville measure. Immediate from conditionalMeasure_apply.
• ★ ProjectiveSector.projectivePreparationLaw_absolutelyContinuous — under a measure bridge π_* muL = c • μFS, the projective preparation law is absolutely continuous w.r.t. μFS. (No c ≠ 0 needed for THIS direction: c • μFS ≪ μFS holds for every c.)
• ★ ProjectiveSector.preparationDensity + projectivePreparationLaw_withDensity — ρ_ep exists: the projective preparation law IS μFS.withDensity ρ_ep with ρ_ep the Radon–Nikodym derivative. The object Papers C and TN2 use, in the corpus for the first time.
• kahlerFstSector + ★★ kahler_preparation_density — the seam corollary at c = 1: on the Kähler arena Σ = ℂℙ^{N-1} × T² with Liouville measure kMuL, the base projection is a ProjectiveSector, its bridge constant is exactly 1 (kahlerFstSector_projectiveLaw), and every region preparation's projective law has a density against THE Fubini–Study measure.
• openBasePreparation + ★★ kahler_preparations_overlap (Q28 item 4b) — the finite-resolution preparation-overlap witness: preparations localised on overlapping projective opens — each an open neighbourhood of its own ray — have conditional measures that are NOT mutually singular (Preparation.conditional_not_mutuallySingular, the item-4a density argument).

⚠️ Scope: the witness is the topological existence form. The quantified "ε-balls around any two states closer than 2ε" form needs a metric on ℙ, which neither Mathlib nor this corpus has (MATHLIB-GAPS.md, Fubini–Study metric row).

References

specs/c2-support-plan.md (items 3–4); SigmaLayer/IsolationPreparation.lean (Preparation, conditional_not_mutuallySingular); SigmaLayer/ProjectiveSector.lean (projectivePreparationLaw); LF4/KahlerInstance.lean (kMuL); LF4/TypicalityForcing.lean (fubiniStudyMeasure_pos_of_isOpen); specs/BACKLOG.md (Q28); specs/future-work.md.

Item 3 — the projective preparation density ρ_ep

theorem CSD.SigmaLayer.Preparation.conditionalMeasure_absolutelyContinuous {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} (P : Preparation D) : (↑P.conditionalMeasure).AbsolutelyContinuous ↑D.muL

The conditional law of a region preparation is absolutely continuous with respect to the Liouville measure: a Liouville-null set stays null after conditioning on the region.

instance CSD.SigmaLayer.instIsProbabilityMeasureProjectivePreparationLaw {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {N : ℕ} {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) : MeasureTheory.IsProbabilityMeasure (Q.projectivePreparationLaw P)

theorem CSD.SigmaLayer.ProjectiveSector.projectivePreparationLaw_absolutelyContinuous {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {N : ℕ} {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) {μFS : MeasureTheory.Measure (ProjectiveState N)} {c : ENNReal} (hbridge : Q.projectiveLaw ↑D.muL = c • μFS) : (Q.projectivePreparationLaw P).AbsolutelyContinuous μFS

★ The projective preparation law is absolutely continuous w.r.t. the Fubini–Study measure, under a measure bridge π_* muL = c • μFS. Note no c ≠ 0 is needed for this direction: c • μFS ≪ μFS for every c.

noncomputable def CSD.SigmaLayer.ProjectiveSector.preparationDensity {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {N : ℕ} {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) (μFS : MeasureTheory.Measure (ProjectiveState N)) : ProjectiveState N → ENNReal

ρ_ep — the projective preparation density: the Radon–Nikodym derivative of the projective preparation law against the reference measure.

Equations

• Q.preparationDensity P μFS = (Q.projectivePreparationLaw P).rnDeriv μFS

theorem CSD.SigmaLayer.ProjectiveSector.projectivePreparationLaw_withDensity {Sigma : Type u_1} [MeasurableSpace Sigma] [Nonempty Sigma] {N : ℕ} {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) {μFS : MeasureTheory.Measure (ProjectiveState N)} [MeasureTheory.SigmaFinite μFS] {c : ENNReal} (hbridge : Q.projectiveLaw ↑D.muL = c • μFS) : μFS.withDensity (Q.preparationDensity P μFS) = Q.projectivePreparationLaw P

★ The projective preparation law IS a density against μFS (Q28 item 3): π_* muH = μFS.withDensity ρ_ep. The missing rung between LF1's region typicality and the projective weights, delivered by Radon–Nikodym.

The Kähler seam at c = 1

def CSD.SigmaLayer.kahlerFstSector {N : ℕ} (D : ConstraintDynamics (LF4.KSigma N)) : ProjectiveSector N D

The base projection of the Kähler arena Σ = ℂℙ^{N-1} × T², as a ProjectiveSector for any dynamics on the arena.

Equations

• CSD.SigmaLayer.kahlerFstSector D = { pi := Prod.fst, measurable_pi := ⋯ }

theorem CSD.SigmaLayer.kahlerFstSector_projectiveLaw {N : ℕ} (p₀ : LF4.CPN N) (D : ConstraintDynamics (LF4.KSigma N)) (hmuL : ↑D.muL = LF4.kMuL p₀) : (kahlerFstSector D).projectiveLaw ↑D.muL = 1 • Matrix.UnitaryGroup.fubiniStudyMeasure p₀

The Kähler bridge constant is exactly 1: the base pushforward of the Liouville measure kMuL = μFS ⊗ vol_{T²} is the Fubini–Study measure.

theorem CSD.SigmaLayer.kahler_preparation_density {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] (D : ConstraintDynamics (LF4.KSigma N)) (hmuL : ↑D.muL = LF4.kMuL p₀) (P : Preparation D) : ((kahlerFstSector D).projectivePreparationLaw P).AbsolutelyContinuous (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ∧ (Matrix.UnitaryGroup.fubiniStudyMeasure p₀).withDensity ((kahlerFstSector D).preparationDensity P (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)) = (kahlerFstSector D).projectivePreparationLaw P

★★ ρ_ep on the Kähler arena (the seam corollary, Q28 item 3): for any dynamics carrying the Liouville measure and any region preparation, the projective preparation law is absolutely continuous against THE Fubini–Study measure and equals μFS.withDensity ρ_ep. The first statement in the corpus connecting SigmaLayer.Preparation to the LF4 measure bridge.

theorem CSD.SigmaLayer.kMuL_fibre_null {N : ℕ} (hN : 2 ≤ N) (p₀ q : LF4.CPN N) : (LF4.kMuL p₀) (Prod.fst ⁻¹' {q}) = 0

★ Single fibres are Liouville-null (via Q28 item 1's atomlessness).

Single projective fibres are kMuL-null, so an exact fibre-supported sharp preparation cannot be obtained by conditioning kMuL on a positive-volume region. Singular exact preparations remain a separate admissible preparation interface — see RecordLayer.no_region_preparation_exact_fibre for this stated as the disjointness of the two classes, and RecordLayer.sharp_preparations_mutuallySingular for that interface's Harrigan–Spekkens classification.

⚠️ Commentary corrected 2026-08-25. This read "the physical story is the region one", which wrongly implied exact sharp measures are illegitimate. They are not; they are singular rather than absolutely continuous, which is a different thing.

Item 4b — overlapping preparations on the Kähler arena

noncomputable def CSD.SigmaLayer.openBasePreparation {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] {V : Set (LF4.CPN N)} (hV : IsOpen V) (hne : V.Nonempty) : Preparation (trivialDynamics ⟨LF4.kMuL p₀, ⋯⟩)

A region preparation carved from a projective open set: the region is the full preimage of a nonempty open V ⊆ ℂℙ^{N-1} under the base projection, with positive Liouville measure by the full support of μFS.

Equations

• CSD.SigmaLayer.openBasePreparation p₀ hV hne = { region := Prod.fst ⁻¹' V, measurable_region := ⋯, nonzero_region := ⋯ }

theorem CSD.SigmaLayer.kahler_preparations_overlap {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] {x y : LF4.CPN N} {Ux Uy : Set (LF4.CPN N)} (hUx : IsOpen Ux) (hUy : IsOpen Uy) (hx : x ∈ Ux) (hy : y ∈ Uy) (hover : (Ux ∩ Uy).Nonempty) : ¬(↑(openBasePreparation p₀ hUx ⋯).conditionalMeasure).MutuallySingular ↑(openBasePreparation p₀ hUy ⋯).conditionalMeasure

★★ The finite-resolution preparation-overlap witness (Q28 item 4b): two preparations, each localised on an open neighbourhood of its own ray, with overlapping neighbourhoods, have conditional measures that are NOT mutually singular. For distinct rays x ≠ y this is the statement that distinct quantum states can be knowledge about overlapping ontic situations — at the level of finite-resolution, region-based preparations.

⚠️ Scope corrected 2026-08-25. This was labelled "the ψ-epistemic overlap witness". Region-preparation overlap does NOT establish Harrigan–Spekkens ψ-epistemicity of exact pure states: that classification is about the exact sharp interface, where the corpus proves ψ-onticity (RecordLayer.sharp_preparations_mutuallySingular). Two different preparation classes, two different claims, both true.