The arena volume is the corpus's μ_FS ⊗ vol_{T²}

TERM-SCOPE(Hamiltonian) — this module uses the restricted sense of "Hamiltonian"; specs/TERMS.md records what is backed and what is not.

Category: 3-Local (the corpus's arena, assembled from Category-1 pieces).

specs/BACKLOG.md ▶ OPEN QUEUE #29 and #32. ArenaSymplectic.lean gave the arena ℂℙᴺ × T² its symplectic form and the top-form measure arenaVolume of arenaForm^(N+1), and proved Liouville for that measure; the record layer's Liouville statements live on the corpus's kMuL = μ_FS ⊗ vol (KahlerInstance.lean). This module identifies the two — first up to the constant that is the arena volume's total mass, by uniqueness rather than by the binomial expansion of the top power (#29), then with the constant computed on one product chart (#32):

• ★ arenaVolume_map_smul — the arena volume is invariant under U(N+1) acting on the sector: the action preserves ω_FS in charts (preservesLocalRep_fsForm_smul), the identity preserves the torus form, and a product of chart-preserving maps preserves the product form and its top power (PreservesLocalRep.prodMap, .wedgePow, .map_topFormMeasure);
• ★ arenaVolume_map_addLeft — the arena volume is invariant under translation of the torus: translation is a chart translation of the translation atlas (AddCircle.isChartTranslation_addLeft), so it preserves the constant area form;
• ★★★ arenaVolume_eq_smul_kMuL — arenaVolume = c · (μ_FS ⊗ vol_{T²}) with c = arenaVolume univ: the sector marginal of the normalised arena volume is a U(N+1)-invariant probability measure, hence μ_FS (fsMeasure_unique); each torus slice is a translation-invariant finite measure on the compact group T², hence a multiple of Haar (isAddInvariant_eq_smul_of_compactSpace); rectangles then determine the product (Measure.prod_eq);
• ★ arenaVolume_chartAt_source — the arena volume of the product chart domain at (origin 0, y₀) is (N+1)·(4π)^N (topFormMeasure_prodTorus_chartAt_source: the flat top power on the product basis is (N+1) times the Fubini–Study coefficient, by the weighted pair-tuple count, and the chart integral factorises through Tonelli); kMuL_chartAt_source — that domain has full kMuL measure (the hyperplane z₀ = 0 and the two cut points are null);
• ★★ arenaVolume_univ — the mass of the arena volume is (N+1)·(4π)^N: the identification reads the total mass off the full-measure chart domain; ★ arenaVolume_ne_zero;
• ★★★ arenaVolume_eq_ofReal_smul_kMuL — arenaVolume = (N+1)·(4π)^N · (μ_FS ⊗ vol_{T²}), with the constant visible, and ★★ kMuL_map_hamiltonianFlow — Liouville for kMuL itself: the Hamiltonian flow of every smooth H on the arena preserves μ_FS ⊗ vol_{T²}, unconditionally.

So Liouville on the arena (arenaVolume_map_hamiltonianFlow) is Liouville for the corpus's kMuL, and the flow of every sector energy, in particular the Schrödinger flow (hamiltonianFlow_sectorEnergy_schrodinger), preserves kMuL as a manifold-level theorem.

Honest scope

⚠️ The constant is convention-bound, exactly as fsVolume_univ's (4π)^N is (ProjectiveSpaceFubiniStudyMass.lean, honest scope): it is the mass of the top power of arenaForm against Lebesgue measure on the model, with fsChartForm's factor -4 and the wedge's own normalisation; the orientation convention is the |·| of topFormMeasure's density.

⚠️ The mass is read off one chart through the identification, not by a null-set argument on the product: topFormMeasure_prodTorus_chartAt_source gives the chart domain, and arenaVolume_eq_smul_kMuL (uniqueness) transports it to the whole arena because the domain has full kMuL measure. The general product identity for top-power measures is still not proved (ProductForm.lean, honest scope).

⚠️ Invariance is proved for the two group actions the identification needs, U(N+1) × id and id × T²; no other symplectomorphism of the arena is read in charts.

References: LF4/ArenaSymplectic.lean (arenaVolume, Liouville on the arena); LF4/KahlerInstance.lean (kMuL); LF4/KahlerVolumeForced.lean (manyToOneSetup_liouville_eq_product); Geometry/Manifold/FormInvariance.lean; Geometry/Manifold/Instances/ProjectiveSpaceTorusVolume.lean (topFormMeasure_prodTorus_chartAt_source); Geometry/Manifold/WedgePowPairs.lean; Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyMass.lean (fsMeasure_chartSource_zero); LinearAlgebra/Projectivization/FubiniStudyUnique.lean (fsMeasure_unique); Mathlib/MeasureTheory/Measure/Haar/Unique.lean; specs/BACKLOG.md (#29, #32); specs/future-work.md.

Finiteness

instance CSD.LF4.isFiniteMeasure_arenaVolume (N : ℕ) : MeasureTheory.IsFiniteMeasure (arenaVolume N)

★ The arena volume is a finite measure (the arena is compact, the density continuous).

The two invariances

theorem CSD.LF4.preservesLocalRep_arenaForm_smul (N : ℕ) (U : ↥(Matrix.unitaryGroup (Fin (N + 1)) ℂ)) : DifferentialForm.PreservesLocalRep (fun (p : KSigma (N + 1)) => (arenaForm N) p) (Prod.map (fun (x : CPN (N + 1)) => U • x) id)

The unitary action on the sector, read on the arena, preserves the arena form in charts.

theorem CSD.LF4.preservesLocalRep_arenaForm_addLeft (N : ℕ) (θ : KTorus) : DifferentialForm.PreservesLocalRep (fun (p : KSigma (N + 1)) => (arenaForm N) p) (Prod.map id fun (y : KTorus) => θ + y)

Translation of the torus, read on the arena, preserves the arena form in charts.

theorem CSD.LF4.arenaVolume_map_smul (N : ℕ) (U : ↥(Matrix.unitaryGroup (Fin (N + 1)) ℂ)) : MeasureTheory.Measure.map (fun (p : KSigma (N + 1)) => U • p) (arenaVolume N) = arenaVolume N

★ The arena volume is invariant under U(N+1) acting on the sector.

theorem CSD.LF4.arenaVolume_map_addLeft (N : ℕ) (θ : KTorus) : MeasureTheory.Measure.map (fun (p : KSigma (N + 1)) => (p.1, θ + p.2)) (arenaVolume N) = arenaVolume N

★ The arena volume is invariant under translation of the torus.

The identification

theorem CSD.LF4.measurable_kSigma_smul (N : ℕ) (U : ↥(Matrix.unitaryGroup (Fin (N + 1)) ℂ)) : Measurable fun (p : KSigma (N + 1)) => U • p

theorem CSD.LF4.measurable_kSigma_addLeft (N : ℕ) (θ : KTorus) : Measurable fun (p : KSigma (N + 1)) => (p.1, θ + p.2)

theorem CSD.LF4.arenaVolume_eq_smul_kMuL (N : ℕ) (p₀ : CPN (N + 1)) : arenaVolume N = (arenaVolume N) Set.univ • kMuL p₀

★★★ The arena volume is the corpus's μ_FS ⊗ vol_{T²} up to its total mass: arenaVolume N = arenaVolume N univ • kMuL p₀, for every base point p₀.

theorem CSD.LF4.kMuL_smul_map_hamiltonianFlow (N : ℕ) (p₀ : CPN (N + 1)) {H : KSigma (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (ArenaModel N)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (t : ℝ) : MeasureTheory.Measure.map (⋯.hamiltonianFlow hH t) ((arenaVolume N) Set.univ • kMuL p₀) = (arenaVolume N) Set.univ • kMuL p₀

★★ Liouville for the corpus's kMuL, at manifold level: the Hamiltonian flow of every smooth H on the arena preserves μ_FS ⊗ vol_{T²} scaled by the arena volume's mass.

The mass

theorem CSD.LF4.arenaVolume_chartAt_source (N : ℕ) (y₀ : KTorus) : (arenaVolume N) (chartAt (ArenaModel N) (Projectivization.origin 0, y₀)).source = ENNReal.ofReal ((↑N + 1) * (4 * Real.pi) ^ N)

★ The arena volume of the product chart domain at (origin 0, y₀) is (N + 1) (4π)^N (topFormMeasure_prodTorus_chartAt_source at T = T' = 1).

theorem CSD.LF4.kMuL_chartAt_source (N : ℕ) (p₀ : CPN (N + 1)) (y₀ : KTorus) : (kMuL p₀) (chartAt (ArenaModel N) (Projectivization.origin 0, y₀)).source = 1

The product chart domain at (origin 0, y₀) has full kMuL measure: the hyperplane z₀ = 0 is μ_FS-null (fsMeasure_chartSource_zero) and the two cut points are vol-null (AddCircle.volume_compl_singleton).

theorem CSD.LF4.arenaVolume_univ (N : ℕ) : (arenaVolume N) Set.univ = ENNReal.ofReal ((↑N + 1) * (4 * Real.pi) ^ N)

★★ The mass of the arena volume is (N + 1) (4π)^N. By the identification arenaVolume_eq_smul_kMuL, the arena volume of a chart domain of full kMuL measure is the total mass.

theorem CSD.LF4.arenaVolume_ne_zero (N : ℕ) : arenaVolume N ≠ 0

★ The arena volume is nonzero.

theorem CSD.LF4.arenaVolume_eq_ofReal_smul_kMuL (N : ℕ) (p₀ : CPN (N + 1)) : arenaVolume N = ENNReal.ofReal ((↑N + 1) * (4 * Real.pi) ^ N) • kMuL p₀

★★★ arenaVolume = (N + 1) (4π)^N · (μ_FS ⊗ vol_{T²}), with the constant visible, for every base point p₀.

theorem CSD.LF4.kMuL_map_hamiltonianFlow (N : ℕ) (p₀ : CPN (N + 1)) {H : KSigma (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (ArenaModel N)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (t : ℝ) : MeasureTheory.Measure.map (⋯.hamiltonianFlow hH t) (kMuL p₀) = kMuL p₀

★★ Liouville for the corpus's kMuL itself, unconditionally: the Hamiltonian flow of every smooth H on the arena preserves μ_FS ⊗ vol_{T²} (the constant of kMuL_smul_map_hamiltonianFlow is nonzero and finite, so it cancels).