The torus stroke is not globally Hamiltonian on the arena: the flux obstruction

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).

R-016″ (specs/BACKLOG.md ▶ OPEN QUEUE #28). LF4/ArenaSymplectic.lean proved the rigid torus stroke (0, a) locally Hamiltonian on the arena (isLocallyHamiltonian_torusStrokeField, d (ι_X ω) = 0). This module proves the other half of the classification RecordLayer/PiecewiseHamiltonian.lean records in the chart, now at manifold level:

• ★★ not_isHamiltonianVectorField_torusStrokeField — for a ≠ 0, no function H on the arena has (0, a) as its Hamiltonian vector field for arenaForm. So the stroke is symplectic and locally Hamiltonian but not Hamiltonian: the flux ∮ dθ ≠ 0 of the withdrawn "piecewise Hamiltonian" reading, as a theorem about the symplectic manifold rather than a remark about a chart.

The argument is the one the row recorded. If ι_{(0,a)} ω = dH, then along every torus direction b the derivative of H is the constant area a b (mfderiv_apply_torus_of_isHamiltonianVectorField): H is then differentiable everywhere (else its derivative would be zero, and a ≠ 0 gives a b with area a b ≠ 0), and along the closed curve s ↦ (x, (θ₁ + s b₁, θ₂ + s b₂)) for s ∈ [0, 1] with b = (1, 0) or (0, 1) the energy H has constant derivative area a b (hasDerivAt_energy_torusCurve), so it changes by area a b over the period (energy_torusCurve_one_sub_zero) while the curve returns to its start (torusCurve_one_eq_zero). Hence −a₂ = 0 and a₁ = 0.

• torusCurve x t₁ t₂ b — the curve; hasMFDerivAt_torusCurve — its manifold derivative is (0, b), from AddCircle.hasMFDerivAt_coe_comp on each circle factor and the self-model pairing lemma;
• arenaForm_torus_pair — arenaForm p ![(0, a), (0, b)] = area a b.

Honest scope

⚠️ H is any function. IsHamiltonianVectorField quantifies over all H : M → ℝ with mfderiv as the derivative (junk 0 where H is not differentiable), so the theorem excludes non-smooth generators too; differentiability of H is derived from the equation.

⚠️ Period 1 only, the corpus's torus. The curve's return uses AddCircle.coe_add_period at T = 1; the argument is the same for any period, restated.

References: LF4/ArenaSymplectic.lean (the arena, torusStrokeField, isLocallyHamiltonian_torusStrokeField); RecordLayer/PiecewiseHamiltonian.lean (the chart-level flux correction this module lifts); Geometry/Manifold/TranslationAtlasForm.lean (AddCircle.hasMFDerivAt_coe_comp); Geometry/Manifold/HamiltonianVectorField.lean (IsHamiltonianVectorField); specs/BACKLOG.md (#28); specs/future-work.md.

The form on two torus vectors, and the derivative of H in a torus direction

theorem CSD.LF4.arenaForm_torus_pair (N : ℕ) (p : KSigma (N + 1)) (a b : ℝ × ℝ) : ((arenaForm N) p) ![(0, a), (0, b)] = TorusForm.area a b

The arena form on two torus vectors is the area form of their torus parts.

theorem CSD.LF4.mfderiv_apply_torus_of_isHamiltonianVectorField {N : ℕ} {a : ℝ × ℝ} {H : KSigma (N + 1) → ℝ} (hH : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (torusStrokeField N a) H) (p : KSigma (N + 1)) (b : ℝ × ℝ) : (mfderiv% H p) (0, b) = TorusForm.area a b

Under ι_{(0,a)} ω = dH, the derivative of H in the torus direction b is area a b, at every point.

theorem CSD.LF4.area_self_rot_pos {a : ℝ × ℝ} (ha : a ≠ 0) : 0 < TorusForm.area a (-a.2, a.1)

A torus direction along which the area pairing with a nonzero a is nonzero.

theorem CSD.LF4.mdifferentiableAt_of_isHamiltonianVectorField_torusStrokeField {N : ℕ} {a : ℝ × ℝ} (ha : a ≠ 0) {H : KSigma (N + 1) → ℝ} (hH : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (torusStrokeField N a) H) (p : KSigma (N + 1)) : MDiffAt H p

Under ι_{(0,a)} ω = dH with a ≠ 0, H is differentiable everywhere: a non-differentiable point would have zero derivative, but the derivative in the direction (−a₂, a₁) is |a|² ≠ 0.

The transverse curve

def CSD.LF4.torusCurve (N : ℕ) (x : CPN (N + 1)) (t₁ t₂ : ℝ) (b : ℝ × ℝ) (s : ℝ) : KSigma (N + 1)

The curve s ↦ (x, (t₁ + s b₁, t₂ + s b₂)) on the arena: the base point fixed, the torus point moving linearly in the direction b.

Equations

• CSD.LF4.torusCurve N x t₁ t₂ b s = (x, ↑(t₁ + s * b.1), ↑(t₂ + s * b.2))

theorem CSD.LF4.torusCurve_one_eq_zero {N : ℕ} (x : CPN (N + 1)) (t₁ t₂ : ℝ) {b : ℝ × ℝ} (hb : b = (1, 0) ∨ b = (0, 1)) : torusCurve N x t₁ t₂ b 1 = torusCurve N x t₁ t₂ b 0

The curve in the direction (1, 0) or (0, 1) returns to its start after time 1: the moving coordinate advances by the period.

theorem CSD.LF4.hasMFDerivAt_torusCurve {N : ℕ} (x : CPN (N + 1)) (t₁ t₂ : ℝ) (b : ℝ × ℝ) (s : ℝ) : HasMFDerivAt% (torusCurve N x t₁ t₂ b) s (ContinuousLinearMap.smulRight 1 (0, b))

The manifold derivative of the curve is (0, b).

The energy along the curve, and the obstruction

theorem CSD.LF4.hasDerivAt_energy_torusCurve {N : ℕ} {a : ℝ × ℝ} (ha : a ≠ 0) {H : KSigma (N + 1) → ℝ} (hH : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (torusStrokeField N a) H) (x : CPN (N + 1)) (t₁ t₂ : ℝ) (b : ℝ × ℝ) (s : ℝ) : HasDerivAt (fun (s : ℝ) => H (torusCurve N x t₁ t₂ b s)) (TorusForm.area a b) s

Under ι_{(0,a)} ω = dH with a ≠ 0, the energy along the curve has constant derivative area a b.

theorem CSD.LF4.energy_torusCurve_one_sub_zero {N : ℕ} {a : ℝ × ℝ} (ha : a ≠ 0) {H : KSigma (N + 1) → ℝ} (hH : DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (torusStrokeField N a) H) (x : CPN (N + 1)) (t₁ t₂ : ℝ) (b : ℝ × ℝ) : H (torusCurve N x t₁ t₂ b 1) - H (torusCurve N x t₁ t₂ b 0) = TorusForm.area a b

Under ι_{(0,a)} ω = dH with a ≠ 0, the energy changes by exactly area a b over one unit of the curve's parameter.

theorem CSD.LF4.not_isHamiltonianVectorField_torusStrokeField {N : ℕ} {a : ℝ × ℝ} (ha : a ≠ 0) (H : KSigma (N + 1) → ℝ) : ¬DifferentialForm.IsHamiltonianVectorField (fun (p : KSigma (N + 1)) => (arenaForm N) p) (torusStrokeField N a) H

★★ The torus stroke is not Hamiltonian on the arena. For a ≠ 0, no function H : KSigma (N+1) → ℝ satisfies ι_{(0,a)} arenaForm = dH: along the closed curves in the directions (1, 0) and (0, 1) such an H would change by −a₂ and by a₁, and it returns to its value. Together with isLocallyHamiltonian_torusStrokeField, the classification "symplectic, locally Hamiltonian, not Hamiltonian" of the strokes, at manifold level.