The arena ℂℙⁿ × T² as a symplectic manifold, and Hamiltonian generation on it

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

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

R-016′ (specs/BACKLOG.md ▶ OPEN QUEUE #7): the arena-level ι_X ω = dH. Until now the programme's arena KSigma (N+1) = ℂℙᴺ × T² was a manifold (Q33, ProjectiveManifold.lean) with no symplectic form, and every "Hamiltonian" statement about a flow on it was either chart-level (RecordLayer/HamiltonianShift.lean) or prose. This module gives the arena its form and states the generator identity on it.

• arenaForm N — the arena's symplectic form π₁^* ω_FS + π₂^* (dθ₁ ∧ dθ₂), a C^∞ 2-form on KSigma (N + 1) over the normed model (Fin N → ℂ) × (ℝ × ℝ) (the product charted on the product normed space, ProductSelfModel.lean; the torus charted by translation, Instances/AddCircleTranslation.lean);
• ★★★ arenaForm_isSymplectic — the arena is a symplectic manifold: the form is closed and non-degenerate, as the sum of the Fubini–Study form and the torus area form (IsSymplectic.prodForm);
• arenaChartCover, arenaBasis, arenaVolume — the finite chart cover, a real basis of the model, and the top-form measure of arenaForm^(N+1);
• ★★ arenaVolume_map_hamiltonianFlow — Liouville on the arena: the Hamiltonian flow of every smooth H : KSigma (N+1) → ℝ preserves arenaVolume, an instance of IsSymplectic.map_hamiltonianFlow_topFormMeasure_wedgePow;
• ★★ isHamiltonianVectorField_sectorEnergy — ι_X ω = dH on the arena for a sector energy: for H : ℂℙᴺ → ℝ with Hamiltonian vector field X on ℂℙᴺ, the field (X, 0) is the Hamiltonian vector field of H ∘ π₁ on the arena; hamiltonianVectorField_sectorEnergy is the uniqueness reading (X_{H∘π₁} = (X_H, 0));
• ★★★ hamiltonianFlow_sectorEnergy — the flow of a sector energy on the arena is the sector's flow with the torus fixed, by uniqueness of integral curves on the compact Hausdorff arena;
• ★★★ hamiltonianFlow_sectorEnergy_schrodinger — the isolated ontic dynamics is a Hamiltonian flow on the arena: the Schrödinger unitary of a Hermitian H, acting on the sector with the torus fixed, is the arena's Hamiltonian flow of −2⟨H⟩ ∘ π₁ (Q29(e) lifted to the arena; A2's vector-field equation, arena level);
• ★★ isLocallyHamiltonian_torusStrokeField — the rigid torus stroke (0, a) is locally Hamiltonian on the arena: ι_{(0,a)} ω is a constant form on the torus factor, so d (ι_X ω) = 0.

Honest scope

⚠️ The arena's measure here is the top-form measure of arenaForm^(N+1). It is the corpus's μ_FS ⊗ vol (LF4/KahlerInstance.lean) up to its total mass: LF4/ArenaVolume.lean proves arenaVolume N = arenaVolume N univ • kMuL p₀ by uniqueness of the invariant measures (arenaVolume_eq_smul_kMuL), so Liouville here is Liouville for kMuL there (kMuL_smul_map_hamiltonianFlow); the mass is (N+1)·(4π)^N (arenaVolume_univ), so the identification holds with its constant visible (arenaVolume_eq_ofReal_smul_kMuL) and Liouville holds for kMuL itself (kMuL_map_hamiltonianFlow).

⚠️ The torus stroke is locally Hamiltonian here; its flux obstruction is the next module. isLocallyHamiltonian_torusStrokeField is the positive half of RecordLayer/PiecewiseHamiltonian.lean's "symplectic, not globally Hamiltonian" at manifold level; the negative half, that no H has (0, a) as its Hamiltonian vector field for a ≠ 0, is LF4/ArenaStrokeFlux.lean (not_isHamiltonianVectorField_torusStrokeField).

⚠️ The measurement propagators are not read on the arena. Nothing here identifies jointLift or hamiltonianShift with a time-1 map of a flow on arenaForm's arena; that identification is the content of the residue this module narrows (⚠️ RESIDUE(R-016)).

References: Geometry/Manifold/ProductForm.lean; Geometry/Manifold/TranslationAtlasForm.lean; Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudySymplectic.lean (fsForm_isSymplectic); Geometry/Manifold/HamiltonianVectorField.lean (IsHamiltonianVectorField, uniqueness); Geometry/Manifold/HamiltonianFlowVolume.lean (Liouville); LF4/ProjectiveManifold.lean (Q33); specs/reconstruction-status.md (A2); specs/BACKLOG.md (R-016′); specs/future-work.md.

@[reducible, inline]

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

The arena's normed model: the model of ℂℙᴺ times the model of the torus.

Equations

• CSD.LF4.ArenaModel N = ((Fin N → ℂ) × ℝ × ℝ)

The arena as a manifold over its normed model

theorem CSD.LF4.ktorus_isManifold_translation : IsManifold (modelWithCornersSelf ℝ (ℝ × ℝ)) ⊤ KTorus

The torus charted by translation, over ℝ × ℝ, is an analytic manifold.

theorem CSD.LF4.ksigma_isManifold_arenaModel (N : ℕ) : IsManifold (modelWithCornersSelf ℝ (ArenaModel N)) ⊤ (KSigma (N + 1))

★ The arena KSigma (N+1) = ℂℙᴺ × T² is an analytic manifold over its normed model, the product charted on the product normed space.

The symplectic form

noncomputable def CSD.LF4.arenaForm (N : ℕ) : DifferentialForm (modelWithCornersSelf ℝ (ArenaModel N)) (KSigma (N + 1)) (↑⊤) (Fin 2) ℝ

The arena's symplectic form π₁^* ω_FS + π₂^* (dθ₁ ∧ dθ₂).

Equations

• CSD.LF4.arenaForm N = Projectivization.fsForm.prodForm AddCircle.torusAreaForm

theorem CSD.LF4.arenaForm_apply (N : ℕ) (p : KSigma (N + 1)) : (arenaForm N) p = (DifferentialForm.toFlat (Projectivization.fsForm p.1)).prodSum TorusForm.areaForm

theorem CSD.LF4.arenaForm_isSymplectic (N : ℕ) : (arenaForm N).IsSymplectic

★★★ The arena is a symplectic manifold.

The chart cover, the basis, and the arena volume

noncomputable def CSD.LF4.arenaChartCover (N : ℕ) : ChartCover (ArenaModel N) (KSigma (N + 1))

A finite cover of the arena by chart domains: the affine charts of ℂℙᴺ times the two translation charts of each circle.

Equations

• CSD.LF4.arenaChartCover N = (Projectivization.affineChartCover N).prod (AddCircle.translationChartCover.prod AddCircle.translationChartCover)

noncomputable def CSD.LF4.arenaBasis (N : ℕ) : Module.Basis (Fin (2 * (N + 1))) ℝ (ArenaModel N)

A real basis of the arena's model, indexed by Fin (2 * (N + 1)): the standard basis of the sector factor followed by the two coordinate vectors of the torus factor (prodTorusBasis, Instances/ProjectiveSpaceTorusVolume.lean).

Equations

• CSD.LF4.arenaBasis N = Projectivization.prodTorusBasis N

noncomputable def CSD.LF4.arenaModelHaar (N : ℕ) : MeasureTheory.Measure (ArenaModel N)

The Haar measure on the arena's model, as the explicit product of the factors' Lebesgue measures (instance search does not see volume on a product as Measure.prod).

Equations

• CSD.LF4.arenaModelHaar N = MeasureTheory.volume.prod (MeasureTheory.volume.prod MeasureTheory.volume)

instance CSD.LF4.instIsAddHaarMeasure_arenaModelHaar (N : ℕ) : (arenaModelHaar N).IsAddHaarMeasure

noncomputable def CSD.LF4.arenaVolume (N : ℕ) : MeasureTheory.Measure (KSigma (N + 1))

The arena volume: the top-form measure of arenaForm^(N+1).

Equations

• One or more equations did not get rendered due to their size.

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

★★ Liouville on the arena. The Hamiltonian flow of every smooth H on the arena preserves the arena volume.

Sector energies: ι_X ω = dH on the arena

def CSD.LF4.sectorEnergy {N : ℕ} (H : CPN (N + 1) → ℝ) : KSigma (N + 1) → ℝ

A function on the sector, read on the arena.

Equations

• CSD.LF4.sectorEnergy H p = H p.1

theorem CSD.LF4.sectorEnergy_apply {N : ℕ} (H : CPN (N + 1) → ℝ) (p : KSigma (N + 1)) : sectorEnergy H p = H p.1

theorem CSD.LF4.contMDiff_sectorEnergy {N : ℕ} {H : CPN (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (Fin N → ℂ)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) : ContMDiff (modelWithCornersSelf ℝ (ArenaModel N)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (sectorEnergy H)

A C^∞ sector energy is C^∞ on the arena.

theorem CSD.LF4.mfderiv_sectorEnergy {N : ℕ} {H : CPN (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (Fin N → ℂ)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (p : KSigma (N + 1)) : mfderiv% (sectorEnergy H) p = mfderiv% H p.1 ∘SL ContinuousLinearMap.fst ℝ (Fin N → ℂ) (ℝ × ℝ)

The derivative of a sector energy on the arena is the derivative on the sector, read on the first component.

theorem CSD.LF4.isHamiltonianVectorField_sectorEnergy {N : ℕ} {H : CPN (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (Fin N → ℂ)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) {X : (x : CPN (N + 1)) → TangentSpace (modelWithCornersSelf ℝ (Fin N → ℂ)) x} (hX : DifferentialForm.IsHamiltonianVectorField (fun (x : Projectivization ℂ (Projectivization.Ambient N)) => Projectivization.fsForm x) X H) : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (fun (p : KSigma (N + 1)) => (X p.1, 0)) (sectorEnergy H)

★★ ι_X ω = dH on the arena for a sector energy. If X is a Hamiltonian vector field of H on ℂℙᴺ for the Fubini–Study form, then (X, 0) is a Hamiltonian vector field of H ∘ π₁ on the arena for arenaForm.

theorem CSD.LF4.hamiltonianVectorField_sectorEnergy {N : ℕ} {H : CPN (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (Fin N → ℂ)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (p : KSigma (N + 1)) : ⋯.hamiltonianVectorField (sectorEnergy H) p = (⋯.hamiltonianVectorField H p.1, 0)

★★ X_{H ∘ π₁} = (X_H, 0): the Hamiltonian vector field of a sector energy on the arena is the sector's Hamiltonian vector field with no torus component (uniqueness for the symplectic arenaForm).

The flow of a sector energy: the sector's flow, the torus fixed

theorem CSD.LF4.isMIntegralCurve_sectorFlow {N : ℕ} {H : CPN (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (Fin N → ℂ)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (x : CPN (N + 1)) (θ : KTorus) : IsMIntegralCurve (fun (t : ℝ) => (⋯.hamiltonianFlow hH t x, θ)) (⋯.hamiltonianVectorField (sectorEnergy H))

The curve t ↦ (flow_H t x, θ) is an integral curve of (X_H, 0) on the arena.

theorem CSD.LF4.hamiltonianFlow_sectorEnergy {N : ℕ} {H : CPN (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (Fin N → ℂ)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (t : ℝ) (x : CPN (N + 1)) (θ : KTorus) : ⋯.hamiltonianFlow ⋯ t (x, θ) = (⋯.hamiltonianFlow hH t x, θ)

★★★ The Hamiltonian flow of a sector energy on the arena is the sector's Hamiltonian flow with the torus fixed: φ^{H∘π₁}_t (x, θ) = (φ^H_t x, θ). Uniqueness of integral curves on the (Hausdorff, compact) arena.

theorem CSD.LF4.hamiltonianFlow_sectorEnergy_schrodinger {N : ℕ} {H : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hH : H.IsHermitian) (t : ℝ) (x : CPN (N + 1)) (θ : KTorus) : ⋯.hamiltonianFlow ⋯ t (x, θ) = (Matrix.schrodingerUnitary hH t • x, θ)

★★★ The isolated ontic dynamics is a Hamiltonian flow on the arena (A2's vector-field equation, arena level): for a Hermitian H, the Hamiltonian flow on ℂℙᴺ × T² of the sector energy −2⟨H⟩ ∘ π₁ is the Schrödinger unitary on the sector with the torus fixed.

The torus stroke: locally Hamiltonian on the arena

def CSD.LF4.torusStrokeField (N : ℕ) (a : ℝ × ℝ) (p : KSigma (N + 1)) : TangentSpace (modelWithCornersSelf ℝ (ArenaModel N)) p

The rigid torus translation field (0, a) on the arena: the generator of the record layer's fibre strokes (RecordLayer/PiecewiseHamiltonian.lean), read on the arena.

Equations

• CSD.LF4.torusStrokeField N a p = (0, a)

theorem CSD.LF4.interiorProduct_arenaForm_torusStrokeField (N : ℕ) (a : ℝ × ℝ) : DifferentialForm.interiorProduct (fun (p : KSigma (N + 1)) => (arenaForm N) p) (torusStrokeField N a) = DifferentialForm.prodFamily (fun (x : CPN (N + 1)) => 0) (DifferentialForm.constFamily (TorusForm.areaForm.curryLeft a))

The interior product ι_{(0,a)} arenaForm is the constant 1-form dθ ↦ area (a, dθ) on the torus factor, pulled back to the arena.

theorem CSD.LF4.isLocallyHamiltonian_torusStrokeField (N : ℕ) (a : ℝ × ℝ) : DifferentialForm.IsLocallyHamiltonian (fun (p : KSigma (N + 1)) => (arenaForm N) p) (torusStrokeField N a)

★★ The torus stroke is locally Hamiltonian on the arena: d (ι_{(0,a)} ω) = 0. Its interior product is a constant form on the torus factor, whose exterior derivative vanishes.