LF4 §8: a non-trivial-fibre compact-Kähler SectorData

Category: 3-Local (a non-trivial-fibre compact-Kähler SectorData).

Glossary: https://glossary.constraintsurfacedynamics.com/fibre/ Plain-language, CSD-role and formal statements of the torus fibre, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Builds the first SectorData with non-trivial fibres, faithful to the Σ0 / Paper A ontology (Σ a finite compact symplectic Kähler space):

Σ = ℂℙ^{N-1} × T²,   T² = (ℝ/ℤ)²   (flat complex torus, compact Kähler);
π = pr₁ : Σ → ℂℙ^{N-1};
μL = μFS ⊗ vol_{T²}   (the product Kähler/Liouville volume);
G = U(N) acting on the base ℂℙ^{N-1}, trivially on the fibre T².

The base ℂℙ^{N-1} carries the quantum-state geometry and the Fubini–Study measure bridge; the fibre T² is the internal ("hidden phase") degree of freedom whose volume fractions realise the Born weights downstream (LF4/SingletKahler.lean). Both factors are genuinely compact Kähler, so Σ is compact Kähler and the flat product volume is its Liouville measure.

Why a torus and not ℂℙ^M. Carving the FS measure on ℂℙ^M into regions of prescribed volume needs the atomless intermediate-value theorem, which is not in Mathlib. (This note used to add "and FS-atomlessness is itself a Haar-of-subgroup argument" — superseded 2026-08-21, Q28 item 1: fubiniStudyMeasure_singleton proves atomlessness by pigeonhole, with no stabiliser Haar measure; the fibres of π are kMuL-null, SigmaLayer/PreparationDensity.lean. The atomless IVT remains the genuinely missing carving ingredient.) The flat torus is equally compact Kähler but its uniform volume carves into arcs elementarily — so the Born-weight regions are genuine flat-Kähler volumes with no measure-isomorphism machinery.

Bridge is axiom-free for this instance. π∗μL = μFS is the product marginal (Measure.fst_prod, c = 1), citing only the foundational triple — invariant_measure_uniqueness is not needed here (cf. LF4/Instance.lean).

Formalisation boundary (honest scope). "Compact Kähler" above is the mathematical reading of these objects, not a formalised structure: in Lean, KSigma is a product type and kMuL a product measure. No manifold structure, symplectic form, or Kähler metric is constructed, and kMuL is not derived from a volume form — Mathlib has no Kähler API, and the corpus does not build one. What is machine-verified is the measure-theoretic content: fubiniStudyMeasure (the Haar-on-U(N) pushforward, which mathematically is the FS Kähler volume), its U(N)-invariance and uniqueness, the product marginal bridge, and everything downstream. The identification of these measures with Kähler/Liouville volume forms is interpretive prose backed by standard differential geometry, not by Lean. Cf. AXIOMS.md §3.1 (preparation-measure origin) for the same boundary stated at the OnticSetup.μL level.

instance CSD.LF4.instFactLtRealOfNat_csdLean4 : Fact (0 < 1)

Fact (0 < 1), needed for AddCircle 1's Haar measure to be a probability measure.

instance CSD.LF4.instProbAddCircleOne : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

AddCircle 1's Haar volume is a probability measure (volume univ = 1).

@[reducible, inline]

abbrev CSD.LF4.KTorus : Type

The flat complex torus T² = (ℝ/ℤ)² (compact Kähler), the internal fibre.

Equations

• CSD.LF4.KTorus = (AddCircle 1 × AddCircle 1)

@[reducible, inline]

abbrev CSD.LF4.KSigma (N : ℕ) : Type

The total ontic space Σ = ℂℙ^{N-1} × T².

Equations

• CSD.LF4.KSigma N = (CSD.LF4.CPN N × CSD.LF4.KTorus)

noncomputable def CSD.LF4.kMuL {N : ℕ} (p₀ : CPN N) : MeasureTheory.Measure (KSigma N)

The product (Kähler/Liouville) volume μL = μFS ⊗ vol_{T²}.

Equations

• CSD.LF4.kMuL p₀ = (Matrix.UnitaryGroup.fubiniStudyMeasure p₀).prod MeasureTheory.volume

instance CSD.LF4.instProbKTorusVolume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

instance CSD.LF4.instProbKMuL {N : ℕ} (p₀ : CPN N) : MeasureTheory.IsProbabilityMeasure (kMuL p₀)

@[instance_reducible]

noncomputable instance CSD.LF4.instSMulKSigma {N : ℕ} : SMul (↥(Matrix.unitaryGroup (Fin N) ℂ)) (KSigma N)

U(N) acts on Σ = ℂℙ^{N-1} × T² through the base factor only.

Equations

• CSD.LF4.instSMulKSigma = { smul := fun (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : CSD.LF4.KSigma N) => (U • p.1, p.2) }

@[simp]

theorem CSD.LF4.kSigma_smul_def {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : KSigma N) : U • p = (U • p.1, p.2)

@[instance_reducible]

noncomputable instance CSD.LF4.instMulActionKSigma {N : ℕ} : MulAction (↥(Matrix.unitaryGroup (Fin N) ℂ)) (KSigma N)

Equations

• CSD.LF4.instMulActionKSigma = { toSMul := CSD.LF4.instSMulKSigma, mul_smul := ⋯, one_smul := ⋯ }

noncomputable def CSD.LF4.kOnticSetup {N : ℕ} [NeZero N] (p₀ : CPN N) : LF1.OnticSetup (KSigma N)

The minimal product OnticSetup: μL is the product Kähler volume, the flow is the identity, the preparation region is everything.

Equations

• CSD.LF4.kOnticSetup p₀ = { μL := ⟨CSD.LF4.kMuL p₀, ⋯⟩, Φ := id, hΦ_pres := ⋯, Ω0 := Set.univ, hΩ0_meas := ⋯, hΩ0_nonzero := ⋯ }

noncomputable def CSD.LF4.kSectorData {N : ℕ} [NeZero N] (p₀ : CPN N) : LF2.SectorData (KSigma N) (CPN N) ↥(Matrix.unitaryGroup (Fin N) ℂ)

Non-trivial-fibre compact-Kähler SectorData. Σ = ℂℙ^{N-1} × T², P = ℂℙ^{N-1}, G = U(N), π = pr₁.

Equations

• CSD.LF4.kSectorData p₀ = { toOntic := CSD.LF4.kOnticSetup p₀, π := Prod.fst, measurable_π := ⋯, measurable_smul_σ := ⋯, measurable_smul_P := ⋯, hμL_inv := ⋯, hπ_equiv := ⋯ }

theorem CSD.LF4.k_measure_bridge {N : ℕ} [NeZero N] (p₀ : CPN N) : ∃ (c : ENNReal), MeasureTheory.Measure.map (kSectorData p₀).π (kSectorData p₀).μL = c • Matrix.UnitaryGroup.fubiniStudyMeasure p₀

Axiom-free measure bridge for the product instance. π∗μL = μFS (c = 1), since the torus volume is a probability measure and π = pr₁.