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:
fsMeasure_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; boundary MOVED 2026-09-10). In this module
KSigma is a product type and kMuL a product measure, and nothing here constructs a
manifold structure, symplectic form, or Kähler metric on them — Mathlib has no Kähler API
(MATHLIB-ABSENT(file:Mathlib/Geometry/Manifold/DifferentialForm)). Since 2026-09-10 the corpus's
own manifold layer supplies exactly that on the base factor, and LF4/SectorManifold.lean proves
kMuL = fsVolumeNormalized n ⊗ Haar with fsVolumeNormalized the normalised top power of the
Fubini–Study form (manyToOneSetup_liouvilleMeasure_eq_fsVolumeNormalized_prod), so kMuL IS
derived from the volume form on the base; the fibre factor stays Haar on T², which is its own
Liouville measure. What this module itself machine-verifies is the measure-theoretic content:
fsMeasure (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.
AddCircle 1's Haar volume is a probability measure (volume univ = 1).
The flat complex torus T² = (ℝ/ℤ)² (compact Kähler), the internal fibre.
Equations
- CSD.LF4.KTorus = (AddCircle 1 × AddCircle 1)
Instances For
The total ontic space Σ = ℂℙ^{N-1} × T².
Equations
Instances For
The product (Kähler/Liouville) volume μL = μFS ⊗ vol_{T²}.
Equations
Instances For
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) }
Equations
- CSD.LF4.instMulActionKSigma = { toSMul := CSD.LF4.instSMulKSigma, mul_smul := ⋯, one_smul := ⋯ }
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 := ⋯ }
Instances For
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 := ⋯ }
Instances For
Axiom-free measure bridge for the product instance. π∗μL = μFS
(c = 1), since the torus volume is a probability measure and π = pr₁.