The echo is a Hamiltonian flow on ℂℙ³ × T² × T²

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

Category: 7-SigmaLayer (the record layer). BACKLOG #202, the generation half (out of #39).

#199 built the echo's dynamics as data on FieldArena 2 2 × (T² × T²). Read on Σ = ℂℙ³ × T² × T² through the index bridge of #195, it is the Hamiltonian flow, for the symplectic form arenaForm ⊕ dψ₁ ∧ dψ₂ of LF4/EchoCoupledFlow.lean, of

−(2/ħ) (J⟨X⟩ + g_A f_A(θ₂ᴬ) n_A + g_B f_B(θ₂ᴮ) n_B),

which is −(2/ħ) times #199's joint energy. The second half of #202: the clock factor is #195's activated_hamiltonian, the echo factor is this file, and the clock-and-echo arena is their product.

• hamOccA, schrodingerHamiltonian_hamOccA — the sender occupancy on Σ's index;
• echoEnergySigma, contMDiff_echoEnergySigma, ★★ echoEnergySigma_eq — the Hamiltonian is −(2/ħ) times #199's joint energy; echoToSigma — the echo arena read on Σ;
• twoCoupledMatrix_eq, reindex_twoDetunedGen, ★★ idxUnitary_twoDetunedFlow — the reindexed two-site detuned exchange is the Schrödinger unitary of A + f_A(θ₂ᴬ) B_A + f_B(θ₂ᴮ) B_B (ODE uniqueness in the matrix algebra); arenaEquiv_twoDetuned_arenaFlow;
• twoAccumA_eq, twoAccumB_eq, ★ echoAmountA_eq, echoAmountB_eq — the pointer displacements of the Hamiltonian flow are #199's lifted displacements;
• ★★★ hamiltonianFlow_echoFlow — the echo is the Hamiltonian flow of its energy, read on Σ; ★ map_hamiltonianFlow_echoFlow — Liouville, inherited from #199 through the identification;
• ★★★ echo_hamiltonian — the package.

References: specs/BACKLOG.md #202, #199, #195, #39; LF4/EchoCoupledFlow.lean, RecordLayer/ActivatedHamiltonian.lean (hamA, hamB, hopIdx, reindexCLM, the proof pattern), RecordLayer/EchoArena.lean, CV/TwoSiteDetuned.lean (twoDetunedGen, occB_twoDetunedFlow).

The sender occupancy on Σ

noncomputable def CSD.RecordLayer.hamOccA (g ħ : ℝ) : Matrix (Fin 4) (Fin 4) ℂ

The sender occupancy, scaled by g/ħ, on Σ's index.

Equations

• CSD.RecordLayer.hamOccA g ħ = (Matrix.reindex CSD.RecordLayer.hopIdx CSD.RecordLayer.hopIdx) (↑(g / ħ) • CSD.CV.occA)

theorem CSD.RecordLayer.occA_isHermitian : CV.occA.IsHermitian

theorem CSD.RecordLayer.hamOccA_isHermitian (g ħ : ℝ) : (hamOccA g ħ).IsHermitian

theorem CSD.RecordLayer.schrodingerHamiltonian_hamOccA (g ħ : ℝ) (p : CV.FieldArena 2 2) : Projectivization.schrodingerHamiltonian (hamOccA g ħ) ((CV.arenaEquiv 2 2) p) = -(2 * g / ħ) * Projectivization.momentMap p CV.excA

The energy on Σ

noncomputable def CSD.RecordLayer.echoEnergySigma (J ħ : ℝ) (A B : PointerCoupling) : LF4.EchoSigma 3 → ℝ

★ The echo's Hamiltonian on Σ: −(2/ħ)(J⟨X⟩ + g_A f_A(θ₂ᴬ) n_A + g_B f_B(θ₂ᴮ) n_B).

Equations

• CSD.RecordLayer.echoEnergySigma J ħ A B = CSD.LF4.twoCoupledEnergy (CSD.RecordLayer.hamA J ħ) (CSD.RecordLayer.hamOccA A.g ħ) (CSD.RecordLayer.hamB B.g ħ) ⋯ ⋯

theorem CSD.RecordLayer.contMDiff_echoEnergySigma (J ħ : ℝ) (A B : PointerCoupling) (hcA : ContDiff ℝ (↑⊤) A.f) (hcB : ContDiff ℝ (↑⊤) B.f) : ContMDiff (modelWithCornersSelf ℝ (LF4.EchoModel 3)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (echoEnergySigma J ħ A B)

noncomputable def CSD.RecordLayer.echoToSigma (x : EchoArena) : LF4.EchoSigma 3

The echo arena read on Σ: the ray through the index bridge, the two tori as they are.

Equations

• CSD.RecordLayer.echoToSigma x = (((CSD.CV.arenaEquiv 2 2) x.1, x.2.1), x.2.2)

theorem CSD.RecordLayer.echoEnergySigma_eq (J ħ : ℝ) (A B : PointerCoupling) (x : EchoArena) : echoEnergySigma J ħ A B (echoToSigma x) = -(2 / ħ) * echoEnergy J A B x

★★ The Hamiltonian is −(2/ħ) times #199's joint energy, read on Σ.

The reindexed two-site exchange is the Schrödinger unitary of the two-angle matrix

theorem CSD.RecordLayer.twoCoupledMatrix_eq (J ħ : ℝ) (A B : PointerCoupling) (φ ψ : AddCircle 1) : LF4.twoCoupledMatrix (hamA J ħ) (hamOccA A.g ħ) (hamB B.g ħ) ⋯ ⋯ φ ψ = (Matrix.reindex hopIdx hopIdx) (↑(1 / ħ) • CV.twoDetunedH J (detuningAt A.g ⋯ φ) (detuningAt B.g ⋯ ψ))

The two-angle matrix is the reindexed two-site detuned Hamiltonian over ħ.

theorem CSD.RecordLayer.reindex_twoDetunedGen (J ħ : ℝ) (A B : PointerCoupling) (φ ψ : AddCircle 1) : (Matrix.reindex hopIdx hopIdx) (CV.twoDetunedGen J ħ (detuningAt A.g ⋯ φ) (detuningAt B.g ⋯ ψ)) = -Complex.I • LF4.twoCoupledMatrix (hamA J ħ) (hamOccA A.g ħ) (hamB B.g ħ) ⋯ ⋯ φ ψ

The reindexed two-site generator, as a multiple of the two-angle matrix.

theorem CSD.RecordLayer.idxUnitary_twoDetunedFlow (J ħ : ℝ) (A B : PointerCoupling) (φ ψ : AddCircle 1) (t : ℝ) : CV.idxUnitary hopIdx ((CV.twoDetunedFlow J ħ (detuningAt A.g ⋯ φ) (detuningAt B.g ⋯ ψ)).flow t) = Matrix.schrodingerUnitary ⋯ t

★★ The reindexed two-site detuned exchange is the Schrödinger unitary of A + f_A(θ₂ᴬ) B_A + f_B(θ₂ᴮ) B_B: both solve U' = −i H U, U 0 = 1.

theorem CSD.RecordLayer.arenaEquiv_twoDetuned_arenaFlow (J ħ : ℝ) (A B : PointerCoupling) (φ ψ : AddCircle 1) (t : ℝ) (p : CV.FieldArena 2 2) : (CV.arenaEquiv 2 2) ((CV.twoDetunedFlow J ħ (detuningAt A.g ⋯ φ) (detuningAt B.g ⋯ ψ)).arenaFlow t p) = Matrix.schrodingerUnitary ⋯ t • (CV.arenaEquiv 2 2) p

The transported ray of the two-site exchange is the two-angle Schrödinger orbit.

The displacements

theorem CSD.RecordLayer.twoAccumA_eq (J ħ : ℝ) (A B : PointerCoupling) (φ ψ : AddCircle 1) (p : CV.FieldArena 2 2) (t : ℝ) : LF4.twoAccumA ⋯ ⋯ ⋯ ⋯ ⋯ φ ψ ((CV.arenaEquiv 2 2) p) t = -(2 * A.g / ħ) * CV.occAccumA J ħ (detuningAt A.g ⋯ φ) (detuningAt B.g ⋯ ψ) p t

The accumulated −2⟨B_A⟩ along the transported orbit is −(2g_A/ħ) times #199's accumulated occupancy of A.

theorem CSD.RecordLayer.twoAccumB_eq (J ħ : ℝ) (A B : PointerCoupling) (φ ψ : AddCircle 1) (p : CV.FieldArena 2 2) (t : ℝ) : LF4.twoAccumB ⋯ ⋯ ⋯ ⋯ ⋯ φ ψ ((CV.arenaEquiv 2 2) p) t = -(2 * B.g / ħ) * CV.occAccum J ħ (detuningAt B.g ⋯ ψ - detuningAt A.g ⋯ φ) p t

The accumulated −2⟨B_B⟩ along the transported orbit is −(2g_B/ħ) times the accumulated occupancy of B.

theorem CSD.RecordLayer.echoAmountA_eq (J ħ : ℝ) (A B : PointerCoupling) (x : EchoArena) (t : ℝ) : ⋯.lift x.2.1.2 * LF4.twoAccumA ⋯ ⋯ ⋯ ⋯ ⋯ x.2.1.2 x.2.2.2 ((CV.arenaEquiv 2 2) x.1) t = echoAmountA J ħ A B t x

★ Pointer A's displacement of the Hamiltonian flow is #199's lifted displacement.

theorem CSD.RecordLayer.echoAmountB_eq (J ħ : ℝ) (A B : PointerCoupling) (x : EchoArena) (t : ℝ) : ⋯.lift x.2.2.2 * LF4.twoAccumB ⋯ ⋯ ⋯ ⋯ ⋯ x.2.1.2 x.2.2.2 ((CV.arenaEquiv 2 2) x.1) t = echoAmountB J ħ A B t x

★ Pointer B's displacement of the Hamiltonian flow is #199's lifted displacement.

The identification

theorem CSD.RecordLayer.hamiltonianFlow_echoFlow (J ħ : ℝ) (A B : PointerCoupling) (hcA : ContDiff ℝ (↑⊤) A.f) (hcB : ContDiff ℝ (↑⊤) B.f) (t : ℝ) (x : EchoArena) : ⋯.hamiltonianFlow ⋯ t (echoToSigma x) = echoToSigma (echoFlow J ħ A B t x)

★★★ The echo is the Hamiltonian flow of its energy. Read on Σ = ℂℙ³ × T² × T² through the index bridge, echoFlow J ħ A B t is hamiltonianFlow (echoEnergySigma J ħ A B) t for the symplectic form arenaForm ⊕ dψ₁ ∧ dψ₂.

theorem CSD.RecordLayer.map_hamiltonianFlow_echoFlow (J ħ : ℝ) (A B : PointerCoupling) (hcA : ContDiff ℝ (↑⊤) A.f) (hcB : ContDiff ℝ (↑⊤) B.f) (t : ℝ) (p₀ : CV.FieldArena 2 2) : MeasureTheory.Measure.map (⋯.hamiltonianFlow ⋯ t) (MeasureTheory.Measure.map echoToSigma ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)) = MeasureTheory.Measure.map echoToSigma ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)

★ Liouville on Σ, inherited from #199 through the identification: the Hamiltonian flow preserves the transported Fubini–Study × Haar⁴ measure.

theorem CSD.RecordLayer.echo_hamiltonian (J ħ : ℝ) (A B : PointerCoupling) (hcA : ContDiff ℝ (↑⊤) A.f) (hcB : ContDiff ℝ (↑⊤) B.f) : ContMDiff (modelWithCornersSelf ℝ (LF4.EchoModel 3)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (echoEnergySigma J ħ A B) ∧ (∀ (t : ℝ) (x : EchoArena), ⋯.hamiltonianFlow ⋯ t (echoToSigma x) = echoToSigma (echoFlow J ħ A B t x)) ∧ (∀ (x : EchoArena), echoEnergySigma J ħ A B (echoToSigma x) = -(2 / ħ) * echoEnergy J A B x) ∧ ∀ (t : ℝ) (p₀ : CV.FieldArena 2 2), MeasureTheory.Measure.map (⋯.hamiltonianFlow ⋯ t) (MeasureTheory.Measure.map echoToSigma ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)) = MeasureTheory.Measure.map echoToSigma ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)

★★★ The echo, generated. On Σ = ℂℙ³ × T² × T² with the symplectic form arenaForm ⊕ dψ₁ ∧ dψ₂: the Hamiltonian −(2/ħ)(J⟨X⟩ + g_A f_A(θ₂ᴬ) n_A + g_B f_B(θ₂ᴮ) n_B) is smooth, its Hamiltonian flow is #199's echoFlow read through the index bridge, the Hamiltonian is −(2/ħ) times #199's joint energy, and the transported Liouville measure is preserved.