The activated write is a 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: 7-SigmaLayer (the record layer). BACKLOG #195 (out of #39; the author's second operational-geometry brief, #191–#197).

#194 built the dynamics of the activated write as data — a two-time, measure-preserving flow on FieldArena 2 2 × T² whose ray runs the detuned exchange and whose pointer obeys θ̇₁ = −(2g/ħ) f'(θ₂) n_B(p(t)). This module identifies it with the Hamiltonian flow of the joint energy on the arena of LF4/ArenaSymplectic.lean (R-016′), through the index bridge FibredFieldArena 2 2 ≃ Σ = ℂℙ³ × T² of CV/ArenaIndexBridge.lean:

𝓗 = −(2/ħ) · (J⟨X⟩ + g f(θ₂) n_B) = coupledEnergy (J X/ħ) (g n_B/ħ) f,

so that activeFlow is hamiltonianFlow 𝓗 read on the field arena — and the pointer rate of #194 is forced: with this corpus's Fubini–Study form the Schrödinger unitary of H is the flow of −2⟨H⟩, and the coupled term inherits the same factor.

• hopIdx, hamA, hamB — the hop and the receiver occupancy, reindexed to Fin 4 and scaled by 1/ħ; hamA_isHermitian, hamB_isHermitian;
• expectation_eq_arenaObs — the two expectation functionals of the corpus agree;
• ★ activatedEnergy, ★★ activatedEnergy_eq — the Hamiltonian is −(2/ħ) times #194's activeEnergy, read on Σ;
• ★★ idxUnitary_detunedFlow — the reindexed detuned exchange is the Schrödinger unitary of A + f(θ₂) B, by the ODE uniqueness of ExpUnique.lean in the matrix algebra; arenaEquiv_arenaFlow;
• schrodingerHamiltonian_hamB, coupledAccum_eq, ★ pointerAmount_eq — the accumulated −2⟨B⟩ along the orbit is the lifted pointer displacement of #194;
• ★★★ hamiltonianFlow_activeFlow — activeFlow is the Hamiltonian flow of 𝓗, transported along the index bridge;
• ★ arenaVolume_map_activeFlow — Liouville for the arena volume of arenaForm^4, as a corollary;
• ★★★ activated_hamiltonian — the package.

Honest scope

• The Hamiltonian is stated with the corpus's normalisation, −(2/ħ) times the row's 𝓗. The row's pointer rate g f'(θ₂) was the naive normalisation; the arena form fixes it to −(2g/ħ) f'(θ₂), and #194's rateAt now carries that factor. Nothing else in #194 changed.
• The identification is along fibredArenaEquiv 2 2, a relabelling of the four configurations; the fibre needs no transport. It is pointwise; the measure statement is the arena's own Liouville theorem read through the relabelling.
• f is C^∞ here (the flow machinery needs a smooth Hamiltonian); #194 needs only C¹.
• The chart-level route (SigmaLayer/UntriggeredFlow.lean) is not taken: the arena route closes the row without the transport boundary R-016 would have left.

References: specs/BACKLOG.md #195, #194, #39; LF4/ArenaCoupledFlow.lean (coupledEnergy, hamiltonianFlow_coupledEnergy); LF4/ArenaSymplectic.lean (arenaForm, arenaVolume_map_hamiltonianFlow); CV/ArenaIndexBridge.lean (arenaEquiv, fibredArenaEquiv, arenaKick_arenaEquiv, arenaObs_arenaEquiv); RecordLayer/ActivatedWrite.lean; Mathlib/Analysis/Normed/Algebra/ExpUnique.lean (exp_smul_eq_of_hasDerivAt).

The expectation functionals agree

theorem CSD.RecordLayer.expectation_eq_arenaObs {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (q : Projectivization ℂ (Projectivization.Ambient n)) : Projectivization.expectation H q = CV.arenaObs H q

The expectation of ProjectiveSpaceSchrodingerFlow.lean is the arena observable of ArenaBridge.lean.

The matrices on Σ

noncomputable def CSD.RecordLayer.hopIdx : CV.HopConfig ≃ Fin 4

The configuration index of the two-site exchange as Fin 4.

Equations

• CSD.RecordLayer.hopIdx = CSD.CV.configEquiv 2 2

noncomputable def CSD.RecordLayer.hamA (J ħ : ℝ) : Matrix (Fin 4) (Fin 4) ℂ

The hop, scaled by 1/ħ, on Σ's index.

Equations

• CSD.RecordLayer.hamA J ħ = (Matrix.reindex CSD.RecordLayer.hopIdx CSD.RecordLayer.hopIdx) (↑(J / ħ) • CSD.CV.hopX)

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

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

Equations

• CSD.RecordLayer.hamB g ħ = (Matrix.reindex CSD.RecordLayer.hopIdx CSD.RecordLayer.hopIdx) (↑(g / ħ) • CSD.CV.occB)

theorem CSD.RecordLayer.arenaObs_reindex_hop (A : Matrix CV.HopConfig CV.HopConfig ℂ) (p : CV.FieldArena 2 2) : CV.arenaObs ((Matrix.reindex hopIdx hopIdx) A) ((CV.arenaEquiv 2 2) p) = CV.arenaObs A p

Arena observables transport along the exchange's relabelling.

theorem CSD.RecordLayer.hopX_isHermitian : CV.hopX.IsHermitian

theorem CSD.RecordLayer.occB_isHermitian : CV.occB.IsHermitian

theorem CSD.RecordLayer.hamA_isHermitian (J ħ : ℝ) : (hamA J ħ).IsHermitian

theorem CSD.RecordLayer.hamB_isHermitian (g ħ : ℝ) : (hamB g ħ).IsHermitian

theorem CSD.RecordLayer.reindex_smul_hop (c : ℂ) (M : Matrix CV.HopConfig CV.HopConfig ℂ) : (Matrix.reindex hopIdx hopIdx) (c • M) = c • (Matrix.reindex hopIdx hopIdx) M

Reindexing is linear: scalars.

theorem CSD.RecordLayer.reindex_add_hop (M N : Matrix CV.HopConfig CV.HopConfig ℂ) : (Matrix.reindex hopIdx hopIdx) (M + N) = (Matrix.reindex hopIdx hopIdx) M + (Matrix.reindex hopIdx hopIdx) N

Reindexing is linear: sums.

noncomputable def CSD.RecordLayer.activatedEnergy {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) : LF4.KSigma 4 → ℝ

★ The Hamiltonian of the activated write on Σ: −(2/ħ)(J⟨X⟩ + g f(θ₂) n_B).

Equations

• CSD.RecordLayer.activatedEnergy J ħ g hf = CSD.LF4.coupledEnergy (CSD.RecordLayer.hamA J ħ) (CSD.RecordLayer.hamB g ħ) hf

theorem CSD.RecordLayer.contMDiff_activatedEnergy {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) : ContMDiff (modelWithCornersSelf ℝ (LF4.ArenaModel 3)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (activatedEnergy J ħ g hf)

theorem CSD.RecordLayer.schrodingerHamiltonian_hamA (J ħ : ℝ) (p : CV.FieldArena 2 2) : Projectivization.schrodingerHamiltonian (hamA J ħ) ((CV.arenaEquiv 2 2) p) = -(2 * J / ħ) * CV.arenaObs CV.hopX p

theorem CSD.RecordLayer.schrodingerHamiltonian_hamB (ħ g : ℝ) (p : CV.FieldArena 2 2) : Projectivization.schrodingerHamiltonian (hamB g ħ) ((CV.arenaEquiv 2 2) p) = -(2 * g / ħ) * Projectivization.momentMap p CV.excB

theorem CSD.RecordLayer.activatedEnergy_eq {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (x : ActiveArena) : activatedEnergy J ħ g hf ((CV.fibredArenaEquiv 2 2) x) = -(2 / ħ) * activeEnergy J g hf x

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

The reindexed detuned exchange is the Schrödinger unitary of A + f(θ₂) B

theorem CSD.RecordLayer.coupledMatrix_eq {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) : LF4.coupledMatrix (hamA J ħ) (hamB g ħ) hf φ = (Matrix.reindex hopIdx hopIdx) (↑(1 / ħ) • CV.detunedH J (detuningAt g hf φ))

The state-dependent matrix of the coupled flow is the reindexed detuned Hamiltonian over ħ.

noncomputable def CSD.RecordLayer.reindexCLM : Matrix CV.HopConfig CV.HopConfig ℂ →L[ℂ] Matrix (Fin 4) (Fin 4) ℂ

The reindexing of matrices, as a continuous linear map.

Equations

• CSD.RecordLayer.reindexCLM = LinearMap.toContinuousLinearMap ↑(Matrix.reindexLinearEquiv ℂ ℂ CSD.RecordLayer.hopIdx CSD.RecordLayer.hopIdx)

@[simp]

theorem CSD.RecordLayer.reindexCLM_apply (M : Matrix CV.HopConfig CV.HopConfig ℂ) : reindexCLM M = (Matrix.reindex hopIdx hopIdx) M

theorem CSD.RecordLayer.reindex_detunedGen {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) : (Matrix.reindex hopIdx hopIdx) (CV.detunedGen J ħ (detuningAt g hf φ)) = -Complex.I • LF4.coupledMatrix (hamA J ħ) (hamB g ħ) hf φ

The reindexed generator, as a multiple of the state-dependent matrix.

theorem CSD.RecordLayer.idxUnitary_detunedFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) (t : ℝ) : CV.idxUnitary hopIdx ((CV.detunedFlow J ħ (detuningAt g hf φ)).flow t) = Matrix.schrodingerUnitary ⋯ t

★★ The reindexed detuned exchange is the Schrödinger unitary of A + f(θ₂) B: both solve U' = −i H U, U 0 = 1 in the matrix algebra, so both are exp (−i t H).

theorem CSD.RecordLayer.arenaEquiv_arenaFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) (t : ℝ) (p : CV.FieldArena 2 2) : (CV.arenaEquiv 2 2) ((CV.detunedFlow J ħ (detuningAt g hf φ)).arenaFlow t p) = Matrix.schrodingerUnitary ⋯ t • (CV.arenaEquiv 2 2) p

The transported ray of the detuned exchange is the Schrödinger orbit of A + f(θ₂) B.

theorem CSD.RecordLayer.coupledAccum_eq {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) (p : CV.FieldArena 2 2) (t : ℝ) : LF4.coupledAccum ⋯ ⋯ hf φ ((CV.arenaEquiv 2 2) p) t = -(2 * g / ħ) * CV.occAccum J ħ (detuningAt g hf φ) p t

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

theorem CSD.RecordLayer.pointerAmount_eq {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (x : ActiveArena) (t : ℝ) : ⋯.lift x.2.2 * LF4.coupledAccum ⋯ ⋯ hf x.2.2 ((CV.arenaEquiv 2 2) x.1) t = pointerAmount J ħ g hf t x

★ The pointer displacement of the Hamiltonian flow is #194's lifted displacement.

theorem CSD.RecordLayer.hamiltonianFlow_activeFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) (t : ℝ) (x : ActiveArena) : ⋯.hamiltonianFlow ⋯ t ((CV.fibredArenaEquiv 2 2) x) = (CV.fibredArenaEquiv 2 2) (activeFlow J ħ g hf t x)

★★★ The activated write is the Hamiltonian flow of its energy. Read on Σ through the index bridge, activeFlow J ħ g hf t is hamiltonianFlow (activatedEnergy J ħ g hf) t for the arena symplectic form.

theorem CSD.RecordLayer.arenaVolume_map_activeFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) (t : ℝ) : MeasureTheory.Measure.map (fun (p : LF4.KSigma 4) => (CV.fibredArenaEquiv 2 2) (activeFlow J ħ g hf t ((CV.fibredArenaEquiv 2 2).symm p))) (LF4.arenaVolume 3) = LF4.arenaVolume 3

★ Liouville on the arena volume for the activated write, read on Σ.

theorem CSD.RecordLayer.activated_hamiltonian {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) : ContMDiff (modelWithCornersSelf ℝ (LF4.ArenaModel 3)) (modelWithCornersSelf ℝ ℝ) (↑⊤) (activatedEnergy J ħ g hf) ∧ (∀ (t : ℝ) (x : ActiveArena), ⋯.hamiltonianFlow ⋯ t ((CV.fibredArenaEquiv 2 2) x) = (CV.fibredArenaEquiv 2 2) (activeFlow J ħ g hf t x)) ∧ (∀ (x : ActiveArena), activatedEnergy J ħ g hf ((CV.fibredArenaEquiv 2 2) x) = -(2 / ħ) * activeEnergy J g hf x) ∧ ∀ (t : ℝ), MeasureTheory.Measure.map (fun (p : LF4.KSigma 4) => (CV.fibredArenaEquiv 2 2) (activeFlow J ħ g hf t ((CV.fibredArenaEquiv 2 2).symm p))) (LF4.arenaVolume 3) = LF4.arenaVolume 3

★★★ The activated write, generated. On Σ = ℂℙ³ × T² with the arena symplectic form: the Hamiltonian −(2/ħ)(J⟨X⟩ + g f(θ₂) n_B) is smooth, its Hamiltonian flow is #194's activeFlow read through the index bridge, the Hamiltonian is −(2/ħ) times #194's joint energy, and the arena volume is preserved.