The Hamiltonian flow of a ray coupled to two tori

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 Kähler arena). BACKLOG #202, the generation half (out of #39).

ArenaCoupledFlow.lean generated the flow of −2⟨A⟩ − 2⟨B⟩ f(θ₂) on ℂℙᴺ × T². The echo of #199 has a pointer at each station, so its arena is ℂℙᴺ × T² × T² and its energy couples the ray to both tori:

𝓗(x, θ, ψ) = −2⟨A⟩(x) − 2⟨B_A⟩(x) f(θ₂) − 2⟨B_B⟩(x) g(ψ₂).

The symplectic form is the product arenaForm ⊕ dψ₁ ∧ dψ₂ (IsSymplectic.prodForm run once more), and the Hamiltonian vector field is the lift of the one-torus field from the first factor plus one more coupled term for the outer torus. The flow is again a skew product over the two conserved angles, in closed form, by uniqueness of integral curves on the compact arena.

• EchoSigma, echoForm, ★ echoForm_isSymplectic — ℂℙᴺ × T² × T² is a symplectic manifold;
• twoCoupledEnergy, contMDiff_twoCoupledEnergy, twoCoupledField;
• ★ isHamiltonianVectorField_fstLift — a Hamiltonian vector field on the arena lifts to the product with the outer torus (the general form of isHamiltonianVectorField_sectorEnergy); ★ isHamiltonianVectorField_outerTerm — the coupled term for the outer torus; ★★ isHamiltonianVectorField_twoCoupled, twoCoupledField_eq_hamiltonianVectorField — ι_X ω = d𝓗 on ℂℙᴺ × T² × T²;
• twoCoupledMatrix, twoAccumA, twoAccumB, twoCoupledCurve, ★★ isMIntegralCurve_twoCoupledCurve; ★★★ hamiltonianFlow_twoCoupledEnergy — the flow in closed form: the Schrödinger unitary of A + f(θ₂) B_A + g(ψ₂) B_B on the ray, θ₁ advanced by f'(θ₂) ∫ (−2⟨B_A⟩), ψ₁ by g'(ψ₂) ∫ (−2⟨B_B⟩), both second angles fixed.

References: specs/BACKLOG.md #202, #199, #195, #39; LF4/ArenaCoupledFlow.lean (the one-torus case, every lemma of which is reused), LF4/ArenaSymplectic.lean, Mathlib/Geometry/Manifold/ProductForm.lean (IsSymplectic.prodForm, prodSum_pair), Mathlib/Geometry/Manifold/IntegralCurve/GlobalFlow.lean.

The echo arena and its symplectic form

@[reducible, inline]

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

The echo arena's normed model: the arena's model times the model of one more torus.

Equations

• CSD.LF4.EchoModel N = (CSD.LF4.ArenaModel N × ℝ × ℝ)

@[reducible, inline]

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

The echo arena ℂℙᴺ × T² × T².

Equations

• CSD.LF4.EchoSigma N = (CSD.LF4.KSigma (N + 1) × CSD.LF4.KTorus)

theorem CSD.LF4.echoSigma_isManifold (N : ℕ) : IsManifold (modelWithCornersSelf ℝ (EchoModel N)) ⊤ (EchoSigma N)

noncomputable def CSD.LF4.echoForm (N : ℕ) : DifferentialForm (modelWithCornersSelf ℝ (EchoModel N)) (EchoSigma N) (↑⊤) (Fin 2) ℝ

The echo arena's symplectic form arenaForm ⊕ dψ₁ ∧ dψ₂.

Equations

• CSD.LF4.echoForm N = (CSD.LF4.arenaForm N).prodForm AddCircle.torusAreaForm

theorem CSD.LF4.echoForm_apply (N : ℕ) (p : EchoSigma N) : (echoForm N) p = (DifferentialForm.toFlat ((arenaForm N) p.1)).prodSum TorusForm.areaForm

theorem CSD.LF4.echoForm_isSymplectic (N : ℕ) : (echoForm N).IsSymplectic

★ ℂℙᴺ × T² × T² is a symplectic manifold.

Lifting a Hamiltonian vector field from the arena to the product

theorem CSD.LF4.isHamiltonianVectorField_fstLift {N : ℕ} {X : (p : KSigma (N + 1)) → TangentSpace (modelWithCornersSelf ℝ (ArenaModel N)) p} {H : KSigma (N + 1) → ℝ} (hH : ContMDiff (modelWithCornersSelf ℝ (ArenaModel N)) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (hX : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) X H) : DifferentialForm.IsHamiltonianVectorField (fun (p : EchoSigma N) => (echoForm N) p) (fun (p : EchoSigma N) => (X p.1, 0)) fun (p : EchoSigma N) => H p.1

★ A Hamiltonian vector field on the arena lifts to the product with the outer torus: if ι_X arenaForm = dH then ι_{(X, 0)} echoForm = d(H ∘ π₁).

The two-torus energy and its field

noncomputable def CSD.LF4.twoCoupledEnergy {N : ℕ} {f g : ℝ → ℝ} (A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (p : EchoSigma N) : ℝ

The two-torus energy −2⟨A⟩ − 2⟨B_A⟩ f(θ₂) − 2⟨B_B⟩ g(ψ₂).

Equations

• CSD.LF4.twoCoupledEnergy A BA BB hf hg p = CSD.LF4.coupledEnergy A BA hf p.1 + Projectivization.schrodingerHamiltonian BB p.1.1 * CSD.LF4.torusPotential hg p.2

theorem CSD.LF4.twoCoupledEnergy_eq {N : ℕ} {f g : ℝ → ℝ} (A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) : twoCoupledEnergy A BA BB hf hg = (fun (p : EchoSigma N) => coupledEnergy A BA hf p.1) + fun (p : EchoSigma N) => Projectivization.schrodingerHamiltonian BB p.1.1 * torusPotential hg p.2

theorem CSD.LF4.contMDiff_outerTerm {N : ℕ} {g : ℝ → ℝ} (BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hg : Function.Periodic g 1) (hcg : ContDiff ℝ (↑⊤) g) : ContMDiff (modelWithCornersSelf ℝ (EchoModel N)) (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (p : EchoSigma N) => Projectivization.schrodingerHamiltonian BB p.1.1 * torusPotential hg p.2

The outer coupled term −2⟨B_B⟩ g(ψ₂) is C^∞ on the echo arena.

theorem CSD.LF4.contMDiff_twoCoupledEnergy {N : ℕ} {f g : ℝ → ℝ} (A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (hc : ContDiff ℝ (↑⊤) f) (hcg : ContDiff ℝ (↑⊤) g) : ContMDiff (modelWithCornersSelf ℝ (EchoModel N)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (twoCoupledEnergy A BA BB hf hg)

The two-torus energy is C^∞ on the echo arena.

noncomputable def CSD.LF4.twoCoupledField {N : ℕ} {f g : ℝ → ℝ} (A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (p : EchoSigma N) : TangentSpace (modelWithCornersSelf ℝ (EchoModel N)) p

The two-torus field: the one-torus coupled field on the arena factor plus g(ψ₂) X_{B_B} on the ray, and (−2⟨B_B⟩ g'(ψ₂), 0) on the outer torus.

Equations

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

theorem CSD.LF4.isHamiltonianVectorField_outerTerm {N : ℕ} {g : ℝ → ℝ} {BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hBB : BB.IsHermitian) (hg : Function.Periodic g 1) (hd : Differentiable ℝ g) : DifferentialForm.IsHamiltonianVectorField (fun (p : EchoSigma N) => (echoForm N) p) (fun (p : EchoSigma N) => ((torusPotential hg p.2 • Projectivization.schrodingerField BB p.1.1, 0), Projectivization.schrodingerHamiltonian BB p.1.1 * ⋯.lift p.2.2, 0)) fun (p : EchoSigma N) => Projectivization.schrodingerHamiltonian BB p.1.1 * torusPotential hg p.2

★ The outer coupled term: ι_X ω = d(−2⟨B_B⟩ g(ψ₂)) on the echo arena for X = ((g(ψ₂) X_{B_B}, 0), (−2⟨B_B⟩ g'(ψ₂), 0)).

theorem CSD.LF4.isHamiltonianVectorField_twoCoupled {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (hc : ContDiff ℝ (↑⊤) f) (hcg : ContDiff ℝ (↑⊤) g) : DifferentialForm.IsHamiltonianVectorField (fun (p : EchoSigma N) => (echoForm N) p) (twoCoupledField A BA BB hf hg) (twoCoupledEnergy A BA BB hf hg)

★★ ι_X ω = d𝓗 on ℂℙᴺ × T² × T² for the two-torus energy.

theorem CSD.LF4.twoCoupledField_eq_hamiltonianVectorField {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (hc : ContDiff ℝ (↑⊤) f) (hcg : ContDiff ℝ (↑⊤) g) : twoCoupledField A BA BB hf hg = ⋯.hamiltonianVectorField (twoCoupledEnergy A BA BB hf hg)

X_𝓗 = twoCoupledField (uniqueness for the symplectic echoForm).

The flow in closed form

noncomputable def CSD.LF4.twoCoupledMatrix {N : ℕ} {f g : ℝ → ℝ} (A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ

The state-dependent matrix at angles (φ, ψ): A + f(φ) B_A + g(ψ) B_B.

Equations

• CSD.LF4.twoCoupledMatrix A BA BB hf hg φ ψ = CSD.LF4.coupledMatrix A BA hf φ + ↑(hg.lift ψ) • BB

theorem CSD.LF4.twoCoupledMatrix_isHermitian {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) : (twoCoupledMatrix A BA BB hf hg φ ψ).IsHermitian

theorem CSD.LF4.schrodingerField_twoCoupledMatrix {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (y : CPN (N + 1)) : Projectivization.schrodingerField (twoCoupledMatrix A BA BB hf hg φ ψ) y = Projectivization.schrodingerField A y + hf.lift φ • Projectivization.schrodingerField BA y + hg.lift ψ • Projectivization.schrodingerField BB y

The Schrödinger field of the two-angle matrix is the combination of the three fields.

theorem CSD.LF4.continuous_twoCoupledOrbit {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) : Continuous fun (s : ℝ) => Matrix.schrodingerUnitary ⋯ s • x

The two-angle Schrödinger orbit from x, as a continuous curve.

theorem CSD.LF4.continuous_schrodingerHamiltonian_twoCoupledOrbit {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (C : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ) (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) : Continuous fun (s : ℝ) => Projectivization.schrodingerHamiltonian C (Matrix.schrodingerUnitary ⋯ s • x)

noncomputable def CSD.LF4.twoAccumA {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) (t : ℝ) : ℝ

The accumulated −2⟨B_A⟩ along the two-angle orbit.

Equations

• CSD.LF4.twoAccumA hA hBA hBB hf hg φ ψ x t = ∫ (s : ℝ) in 0..t, Projectivization.schrodingerHamiltonian BA (Matrix.schrodingerUnitary ⋯ s • x)

noncomputable def CSD.LF4.twoAccumB {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) (t : ℝ) : ℝ

The accumulated −2⟨B_B⟩ along the two-angle orbit.

Equations

• CSD.LF4.twoAccumB hA hBA hBB hf hg φ ψ x t = ∫ (s : ℝ) in 0..t, Projectivization.schrodingerHamiltonian BB (Matrix.schrodingerUnitary ⋯ s • x)

theorem CSD.LF4.twoAccumA_zero {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) : twoAccumA hA hBA hBB hf hg φ ψ x 0 = 0

theorem CSD.LF4.twoAccumB_zero {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) : twoAccumB hA hBA hBB hf hg φ ψ x 0 = 0

theorem CSD.LF4.hasDerivAt_twoAccumA {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) (t : ℝ) : HasDerivAt (fun (t : ℝ) => twoAccumA hA hBA hBB hf hg φ ψ x t) (Projectivization.schrodingerHamiltonian BA (Matrix.schrodingerUnitary ⋯ t • x)) t

theorem CSD.LF4.hasDerivAt_twoAccumB {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (φ ψ : AddCircle 1) (x : CPN (N + 1)) (t : ℝ) : HasDerivAt (fun (t : ℝ) => twoAccumB hA hBA hBB hf hg φ ψ x t) (Projectivization.schrodingerHamiltonian BB (Matrix.schrodingerUnitary ⋯ t • x)) t

noncomputable def CSD.LF4.twoCoupledCurve {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (x : CPN (N + 1)) (a₀ : ℝ) (φ : AddCircle 1) (b₀ : ℝ) (ψ : AddCircle 1) (t : ℝ) : EchoSigma N

The closed-form curve: the two-angle orbit, θ₁ = a₀ + f'(φ) ∫ (−2⟨B_A⟩), θ₂ = φ, ψ₁ = b₀ + g'(ψ) ∫ (−2⟨B_B⟩), ψ₂ = ψ.

Equations

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

theorem CSD.LF4.isMIntegralCurve_twoCoupledCurve {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (hc : ContDiff ℝ (↑⊤) f) (hcg : ContDiff ℝ (↑⊤) g) (x : CPN (N + 1)) (a₀ : ℝ) (φ : AddCircle 1) (b₀ : ℝ) (ψ : AddCircle 1) : IsMIntegralCurve (twoCoupledCurve hA hBA hBB hf hg x a₀ φ b₀ ψ) (⋯.hamiltonianVectorField (twoCoupledEnergy A BA BB hf hg))

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

theorem CSD.LF4.hamiltonianFlow_twoCoupledEnergy {N : ℕ} {f g : ℝ → ℝ} {A BA BB : Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ} (hA : A.IsHermitian) (hBA : BA.IsHermitian) (hBB : BB.IsHermitian) (hf : Function.Periodic f 1) (hg : Function.Periodic g 1) (hc : ContDiff ℝ (↑⊤) f) (hcg : ContDiff ℝ (↑⊤) g) (t : ℝ) (x : CPN (N + 1)) (θ ψ : KTorus) : ⋯.hamiltonianFlow ⋯ t ((x, θ), ψ) = ((Matrix.schrodingerUnitary ⋯ t • x, θ.1 + ↑(⋯.lift θ.2 * twoAccumA hA hBA hBB hf hg θ.2 ψ.2 x t), θ.2), ψ.1 + ↑(⋯.lift ψ.2 * twoAccumB hA hBA hBB hf hg θ.2 ψ.2 x t), ψ.2)

★★★ The Hamiltonian flow of the two-torus energy in closed form: the Schrödinger unitary of A + f(θ₂) B_A + g(ψ₂) B_B on the ray, θ₁ advanced by f'(θ₂) ∫ (−2⟨B_A⟩), ψ₁ by g'(ψ₂) ∫ (−2⟨B_B⟩), both second angles fixed — a skew product over the two conserved angles.