A sector energy coupled to a torus angle: the Hamiltonian flow on the arena

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). BACKLOG #195.

ArenaSymplectic.lean handles energies of one factor: a sector energy's flow is the sector's flow with the torus fixed. This module handles the first energy coupling the two factors,

𝓗(x, θ) = −2⟨A⟩(x) − 2⟨B⟩(x) · f(θ₂), A, B Hermitian, f smooth of period 1,

the arena form being π₁^* ω_FS + π₂^* (dθ₁ ∧ dθ₂). Hamilton's equations split as the row says: at fixed θ₂ the ray sees the state-dependent Hermitian matrix A + f(θ₂) B, so it runs that Schrödinger unitary; θ₂ is conserved (𝓗 does not depend on θ₁); and θ₁ moves at the rate −2⟨B⟩(x) f'(θ₂) — only while ⟨B⟩ is nonzero on the orbit. The flow is a skew product, in closed form.

• expectation_add, expectation_real_smul, schrodingerHamiltonian_add, schrodingerHamiltonian_real_smul, ★ schrodingerField_add_real_smul — the Schrödinger field is linear in the matrix, by uniqueness of Hamiltonian vector fields for the symplectic Fubini–Study form;
• torusPotential, ★ isHamiltonianVectorField_torusPotential — the Hamiltonian vector field of f(θ₂) for the area form is (f'(θ₂), 0), from the periodic-lift calculus of AddCirclePeriodicLift.lean;
• coupledEnergy, coupledField, ★★ isHamiltonianVectorField_coupled — ι_X ω = d𝓗 on the arena for the coupled energy, with X = (X_A + f(θ₂) X_B, (−2⟨B⟩ f'(θ₂), 0)); this is the coupled product field the row was stuck on, obtained from the product rule for mfderiv and the factorwise pairing prodSum_pair; coupledField_eq_hamiltonianVectorField;
• coupledMatrix, coupledAccum, coupledCurve, ★★ isMIntegralCurve_coupledCurve — the closed-form curve is an integral curve: the detuned Schrödinger orbit, θ₁ advanced by f'(θ₂) ∫₀ᵗ (−2⟨B⟩) along it, θ₂ fixed;
• ★★★ hamiltonianFlow_coupledEnergy — the Hamiltonian flow of the coupled energy in closed form, by uniqueness of integral curves on the compact arena;
• ★ arenaVolume_map_coupledFlow — Liouville for it, read off the explicit map.

Honest scope

• The sector is ℂℙᴺ with Mathlib's Fin (N+1) index; the record layer's field arenas reach it through the index bridge (CV/ArenaIndexBridge.lean), which is where #194's flow is identified with this one (RecordLayer/ActivatedHamiltonian.lean).
• The normalisation is the corpus's: with this Fubini–Study form the Schrödinger unitary of H is the flow of −2⟨H⟩ (hamiltonianFlow_schrodingerHamiltonian), so the coupled term carries the same −2, and the pointer rate is −2⟨B⟩ f'(θ₂). No other normalisation is claimed.
• f is C^∞ where the flow is taken (the Hamiltonian must be smooth for the flow machinery); C^1 suffices for the vector-field identity.

References: LF4/ArenaSymplectic.lean (arenaForm, sectorEnergy, isHamiltonianVectorField_sectorEnergy, hamiltonianFlow_sectorEnergy); Geometry/Manifold/Instances/ProjectiveSpaceSchrodingerFlow.lean (schrodingerField, schrodingerField_isHamiltonianVectorField, isMIntegralCurve_schrodingerUnitary_smul); Geometry/Manifold/Instances/AddCirclePeriodicLift.lean; Geometry/Manifold/ProductForm.lean (prodSum_pair); Geometry/Manifold/IntegralCurve/GlobalFlow.lean (integralFlow_eq_of_isMIntegralCurve); specs/BACKLOG.md #195, #194.

Linearity of the Schrödinger Hamiltonian and field in the matrix

theorem CSD.LF4.expectation_add {N : ℕ} (A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (p : CPN (N + 1)) : Projectivization.expectation (A + B) p = Projectivization.expectation A p + Projectivization.expectation B p

theorem CSD.LF4.expectation_real_smul {N : ℕ} (c : ℝ) (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (p : CPN (N + 1)) : Projectivization.expectation (↑c • A) p = c * Projectivization.expectation A p

theorem CSD.LF4.schrodingerHamiltonian_add {N : ℕ} (A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) : Projectivization.schrodingerHamiltonian (A + B) = Projectivization.schrodingerHamiltonian A + Projectivization.schrodingerHamiltonian B

theorem CSD.LF4.schrodingerHamiltonian_real_smul {N : ℕ} (c : ℝ) (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) : Projectivization.schrodingerHamiltonian (↑c • A) = c • Projectivization.schrodingerHamiltonian A

theorem CSD.LF4.mdifferentiableAt_schrodingerHamiltonian {N : ℕ} (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (x : CPN (N + 1)) : MDiffAt (Projectivization.schrodingerHamiltonian A) x

theorem CSD.LF4.isHermitian_add_real_smul {N : ℕ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (c : ℝ) : (A + ↑c • B).IsHermitian

theorem CSD.LF4.schrodingerField_add_real_smul {N : ℕ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (c : ℝ) (x : CPN (N + 1)) : Projectivization.schrodingerField (A + ↑c • B) x = Projectivization.schrodingerField A x + c • Projectivization.schrodingerField B x

★ The Schrödinger field is linear in the matrix: the field of A + c B is the combination of the fields, by uniqueness of Hamiltonian vector fields for the symplectic fsForm.

The torus potential f(θ₂) and its Hamiltonian vector field

def CSD.LF4.torusPotential {f : ℝ → ℝ} (hf : Function.Periodic f 1) (θ : KTorus) : ℝ

The second torus angle read through a periodic potential.

Equations

• CSD.LF4.torusPotential hf θ = hf.lift θ.2

theorem CSD.LF4.hasMFDerivAt_torusPotential {f : ℝ → ℝ} (hf : Function.Periodic f 1) (hd : Differentiable ℝ f) (θ : KTorus) : HasMFDerivAt% (torusPotential hf) θ (ContinuousLinearMap.smulRight 1 (⋯.lift θ.2) ∘SL ContinuousLinearMap.snd ℝ ℝ ℝ)

theorem CSD.LF4.contMDiff_torusPotential {f : ℝ → ℝ} (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) : ContMDiff (modelWithCornersSelf ℝ (ℝ × ℝ)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (torusPotential hf)

theorem CSD.LF4.isHamiltonianVectorField_torusPotential {f : ℝ → ℝ} (hf : Function.Periodic f 1) (hd : Differentiable ℝ f) : DifferentialForm.IsHamiltonianVectorField (fun (θ : KTorus) => AddCircle.torusAreaForm θ) (fun (θ : KTorus) => (⋯.lift θ.2, 0)) (torusPotential hf)

★ The Hamiltonian vector field of f(θ₂) for the area form dθ₁ ∧ dθ₂ is (f'(θ₂), 0).

The coupled energy and its Hamiltonian vector field

noncomputable def CSD.LF4.coupledEnergy {N : ℕ} {f : ℝ → ℝ} (A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (p : KSigma (N + 1)) : ℝ

The coupled energy −2⟨A⟩(x) − 2⟨B⟩(x) f(θ₂) on the arena.

Equations

• CSD.LF4.coupledEnergy A B hf p = Projectivization.schrodingerHamiltonian A p.1 + Projectivization.schrodingerHamiltonian B p.1 * CSD.LF4.torusPotential hf p.2

theorem CSD.LF4.coupledEnergy_eq {N : ℕ} {f : ℝ → ℝ} (A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) : coupledEnergy A B hf = sectorEnergy (Projectivization.schrodingerHamiltonian A) + fun (p : KSigma (N + 1)) => Projectivization.schrodingerHamiltonian B p.1 * torusPotential hf p.2

theorem CSD.LF4.contMDiff_torusPotential_snd {N : ℕ} {f : ℝ → ℝ} (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) : ContMDiff (modelWithCornersSelf ℝ (ArenaModel N)) (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (p : KSigma (N + 1)) => torusPotential hf p.2

theorem CSD.LF4.contMDiff_coupledEnergy {N : ℕ} {f : ℝ → ℝ} (A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) : ContMDiff (modelWithCornersSelf ℝ (ArenaModel N)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (coupledEnergy A B hf)

The coupled energy is C^∞ on the arena.

noncomputable def CSD.LF4.coupledField {N : ℕ} {f : ℝ → ℝ} (A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (p : KSigma (N + 1)) : TangentSpace (modelWithCornersSelf ℝ (ArenaModel N)) p

The coupled field (X_A + f(θ₂) X_B, (−2⟨B⟩ f'(θ₂), 0)).

Equations

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

theorem CSD.LF4.isHamiltonianVectorField_coupledTerm {N : ℕ} {f : ℝ → ℝ} {B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hB : B.IsHermitian) (hf : Function.Periodic f 1) (hd : Differentiable ℝ f) : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (fun (p : KSigma (N + 1)) => (torusPotential hf p.2 • Projectivization.schrodingerField B p.1, Projectivization.schrodingerHamiltonian B p.1 * ⋯.lift p.2.2, 0)) fun (p : KSigma (N + 1)) => Projectivization.schrodingerHamiltonian B p.1 * torusPotential hf p.2

The coupled term alone: ι_X ω = d (−2⟨B⟩ · f(θ₂)) on the arena for X = (f(θ₂) X_B, (−2⟨B⟩ f'(θ₂), 0)).

theorem CSD.LF4.isHamiltonianVectorField_coupled {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (hd : Differentiable ℝ f) : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (coupledField A B hf) (coupledEnergy A B hf)

★★ ι_X ω = d𝓗 on the arena for the coupled energy. The coupled product field the row was stuck on: the sector energy's field with the torus fixed, plus the coupled term's field.

theorem CSD.LF4.coupledField_eq_hamiltonianVectorField {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (hd : Differentiable ℝ f) : coupledField A B hf = ⋯.hamiltonianVectorField (coupledEnergy A B hf)

X_𝓗 = coupledField: the Hamiltonian vector field of the coupled energy is the coupled field (uniqueness for the symplectic arenaForm).

The flow in closed form

def CSD.LF4.coupledMatrix {N : ℕ} {f : ℝ → ℝ} (A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (φ : AddCircle 1) : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ

The state-dependent matrix at angle φ: A + f(φ) B.

Equations

• CSD.LF4.coupledMatrix A B hf φ = A + ↑(hf.lift φ) • B

theorem CSD.LF4.coupledMatrix_isHermitian {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (φ : AddCircle 1) : (coupledMatrix A B hf φ).IsHermitian

theorem CSD.LF4.schrodingerField_coupledMatrix {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (φ : AddCircle 1) (y : CPN (N + 1)) : Projectivization.schrodingerField (coupledMatrix A B hf φ) y = Projectivization.schrodingerField A y + hf.lift φ • Projectivization.schrodingerField B y

The Schrödinger field of the state-dependent matrix is the combination of the fields.

theorem CSD.LF4.continuous_coupledOrbit {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (φ : AddCircle 1) (x : CPN (N + 1)) : Continuous fun (s : ℝ) => Matrix.schrodingerUnitary ⋯ s • x

The detuned Schrödinger orbit from x at angle φ, as a continuous curve.

theorem CSD.LF4.continuous_schrodingerHamiltonian_coupledOrbit {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (φ : AddCircle 1) (x : CPN (N + 1)) : Continuous fun (s : ℝ) => Projectivization.schrodingerHamiltonian B (Matrix.schrodingerUnitary ⋯ s • x)

The integrand −2⟨B⟩ along the orbit is continuous.

noncomputable def CSD.LF4.coupledAccum {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (φ : AddCircle 1) (x : CPN (N + 1)) (t : ℝ) : ℝ

The accumulated −2⟨B⟩ along the detuned orbit.

Equations

• CSD.LF4.coupledAccum hA hB hf φ x t = ∫ (s : ℝ) in 0..t, Projectivization.schrodingerHamiltonian B (Matrix.schrodingerUnitary ⋯ s • x)

theorem CSD.LF4.coupledAccum_zero {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (φ : AddCircle 1) (x : CPN (N + 1)) : coupledAccum hA hB hf φ x 0 = 0

theorem CSD.LF4.hasDerivAt_coupledAccum {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (φ : AddCircle 1) (x : CPN (N + 1)) (t : ℝ) : HasDerivAt (fun (t : ℝ) => coupledAccum hA hB hf φ x t) (Projectivization.schrodingerHamiltonian B (Matrix.schrodingerUnitary ⋯ t • x)) t

noncomputable def CSD.LF4.coupledCurve {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (x : CPN (N + 1)) (a₀ : ℝ) (φ : AddCircle 1) (t : ℝ) : KSigma (N + 1)

The closed-form curve: the detuned orbit, θ₁ = a₀ + f'(φ) ∫₀ᵗ (−2⟨B⟩), θ₂ = φ.

Equations

• CSD.LF4.coupledCurve hA hB hf x a₀ φ t = (Matrix.schrodingerUnitary ⋯ t • x, ↑(a₀ + ⋯.lift φ * CSD.LF4.coupledAccum hA hB hf φ x t), φ)

theorem CSD.LF4.isMIntegralCurve_coupledCurve {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (hd : Differentiable ℝ f) (x : CPN (N + 1)) (a₀ : ℝ) (φ : AddCircle 1) : IsMIntegralCurve (coupledCurve hA hB hf x a₀ φ) (⋯.hamiltonianVectorField (coupledEnergy A B hf))

★★ The closed-form curve is an integral curve of the coupled field.

theorem CSD.LF4.hamiltonianFlow_coupledEnergy {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) (t : ℝ) (x : CPN (N + 1)) (θ : KTorus) : ⋯.hamiltonianFlow ⋯ t (x, θ) = (Matrix.schrodingerUnitary ⋯ t • x, θ.1 + ↑(⋯.lift θ.2 * coupledAccum hA hB hf θ.2 x t), θ.2)

★★★ The Hamiltonian flow of the coupled energy in closed form. At (x, θ) the flow for time t is the Schrödinger unitary of A + f(θ₂) B on the sector, the angle θ₁ advanced by f'(θ₂) ∫₀ᵗ (−2⟨B⟩) along that orbit, and θ₂ unchanged — a skew product over the conserved angle, by uniqueness of integral curves on the compact arena.

theorem CSD.LF4.arenaVolume_map_coupledFlow {N : ℕ} {f : ℝ → ℝ} {A B : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) (t : ℝ) : MeasureTheory.Measure.map (fun (p : KSigma (N + 1)) => (Matrix.schrodingerUnitary ⋯ t • p.1, p.2.1 + ↑(⋯.lift p.2.2 * coupledAccum hA hB hf p.2.2 p.1 t), p.2.2)) (arenaVolume N) = arenaVolume N

★ Liouville for the coupled flow, read off the explicit map.