SigmaLayer/ChartBracket: the Poisson bracket in a Darboux chart, and why the weights commute

Category: 7-SigmaLayer (dynamical measurement) — specs/BACKLOG.md A3, the formalisable fragment of the joint-arena Hamiltonian argument.

What this is for

The joint-arena route (BACKLOG.md A2) turns on one algebraic step: the control weights Poisson-commute, hence are constants of motion of the true joint flow, hence the pointer sees the fixed weight vector the existing analysis assumes. Stating that on the arena needs ω⁻¹dH and a manifold Poisson bracket on the ARENA. ω⁻¹dH exists on ℂℙⁿ since 2026-09-08 (DifferentialForm.hamiltonianVectorField, HamiltonianVectorField.lean; the Poisson bracket of two Hamiltonians is ω(X_H, X_K), not yet named); the arena's product form and the bracket on it are R-016′ (BACKLOG.md ▶ OUTSTANDING, L). Mathlib itself still has none of it (MATHLIB-ABSENT(file:Mathlib/Geometry/Manifold/DifferentialForm)).

What is expressible, and is proved here, is the same step in a Darboux chart: on (Fin n → ℝ) × (Fin n → ℝ) with canonical coordinates, the bracket is an explicit fderiv expression, the Hamiltonian vector field is explicit (no ω⁻¹ needed — in canonical coordinates it is (∂_y H, −∂_x H)), and the vanishing argument is a computation.

The statement that matters, and why it is not the obvious one

The naive reading — "the weights and 𝓗 are both independent of the momenta, so they commute" — is false of 𝓗. The interaction scalar 𝓗 = Σⱼ wⱼ(x)hⱼ(q) depends on the pointer, momenta included. What is true, and what poissonBracket_eq_zero_of_disjoint proves, is a disjoint-support statement:

if f has no momentum dependence at all, and every position index f depends on is disjoint from every momentum index g depends on, then {f, g} = 0.

That is exactly the corpus's situation: the weights depend on base positions (the moment coordinates and the register angle θ₁), while 𝓗's momentum dependence is carried by the pointer's conjugate variables — different indices. The bracket vanishes because the supports are disjoint, not because 𝓗 is momentum-free.

Results

• poissonBracket — the canonical bracket, via fderiv on basis directions.
• ★ poissonBracket_eq_zero_of_disjoint — the vanishing theorem above.
• poissonBracket_comm_of_momentumIndep — two momentum-free functions always commute (the special case for weights against each other, {wᵢ,wⱼ} = 0).
• hamiltonianField — (∂_y H, −∂_x H), explicit in canonical coordinates.
• ★ conserved_of_bracket_eq_zero — a function with vanishing bracket against H is constant along any integral curve of X_H: the conservation conclusion A2 needs.

⚠️ Honest scope. This is a chart model, deliberately: KSigma N × ℂℙ^K is not globally ℝ^{2n}, and nothing here transports the result to the arena — that transport is the missing arrow. So this machine-checks A2's algebra, not A2. It also says nothing about whether the corpus's weights satisfy the hypotheses as functions on the arena; what makes that plausible is that the weights are C^∞ in the register coordinate (contDiff_pointerWeights_lift: the universal-cover lift at fixed base point and rates) and depend only on the moment coordinates and θ₁ (pointerWeights). Finally, dω = 0 is not stated: in a canonical chart it is automatic, which is precisely why a chart model is weaker than the manifold statement.

References

specs/BACKLOG.md A2 (the paper argument this supports), A3 (this row), A4 (the blocked arrow); RecordLayer/JointFlowTransfer.lean (A1 — what conservation is for); RecordLayer/PointerWeights.lean (pointerWeights, contDiff_pointerWeights_lift); Mathlib/Analysis/InnerProductSpace/KahlerForm.lean (the pointwise Kähler triple, the form-level analogue).

@[reducible, inline]

abbrev CSD.SigmaLayer.Chart (n : ℕ) : Type

A Darboux chart: n positions and n conjugate momenta.

Equations

• CSD.SigmaLayer.Chart n = ((Fin n → ℝ) × (Fin n → ℝ))

def CSD.SigmaLayer.posDir {n : ℕ} (i : Fin n) : Chart n

The i-th position direction.

Equations

• CSD.SigmaLayer.posDir i = (Pi.single i 1, 0)

def CSD.SigmaLayer.momDir {n : ℕ} (i : Fin n) : Chart n

The i-th momentum direction.

Equations

• CSD.SigmaLayer.momDir i = (0, Pi.single i 1)

noncomputable def CSD.SigmaLayer.dPos {n : ℕ} (f : Chart n → ℝ) (z : Chart n) (i : Fin n) : ℝ

∂f/∂xᵢ at z.

Equations

• CSD.SigmaLayer.dPos f z i = (fderiv ℝ f z) (CSD.SigmaLayer.posDir i)

noncomputable def CSD.SigmaLayer.dMom {n : ℕ} (f : Chart n → ℝ) (z : Chart n) (i : Fin n) : ℝ

∂f/∂yᵢ at z.

Equations

• CSD.SigmaLayer.dMom f z i = (fderiv ℝ f z) (CSD.SigmaLayer.momDir i)

noncomputable def CSD.SigmaLayer.poissonBracket {n : ℕ} (f g : Chart n → ℝ) (z : Chart n) : ℝ

The canonical Poisson bracket {f,g} = Σᵢ (∂ₓᵢf ∂yᵢg − ∂yᵢf ∂ₓᵢg).

Equations

• CSD.SigmaLayer.poissonBracket f g z = ∑ i : Fin n, (CSD.SigmaLayer.dPos f z i * CSD.SigmaLayer.dMom g z i - CSD.SigmaLayer.dMom f z i * CSD.SigmaLayer.dPos g z i)

Dependence predicates

def CSD.SigmaLayer.MomentumIndep {n : ℕ} (f : Chart n → ℝ) : Prop

f has no momentum dependence.

Equations

• CSD.SigmaLayer.MomentumIndep f = ∀ (z : CSD.SigmaLayer.Chart n) (i : Fin n), CSD.SigmaLayer.dMom f z i = 0

def CSD.SigmaLayer.PositionSupport {n : ℕ} (f : Chart n → ℝ) (S : Finset (Fin n)) : Prop

Every position index f depends on lies in S.

Equations

• CSD.SigmaLayer.PositionSupport f S = ∀ (z : CSD.SigmaLayer.Chart n), ∀ i ∉ S, CSD.SigmaLayer.dPos f z i = 0

def CSD.SigmaLayer.MomentumSupport {n : ℕ} (g : Chart n → ℝ) (T : Finset (Fin n)) : Prop

Every momentum index g depends on lies in T.

Equations

• CSD.SigmaLayer.MomentumSupport g T = ∀ (z : CSD.SigmaLayer.Chart n), ∀ i ∉ T, CSD.SigmaLayer.dMom g z i = 0

★ The vanishing theorem

theorem CSD.SigmaLayer.poissonBracket_eq_zero_of_disjoint {n : ℕ} {f g : Chart n → ℝ} {S T : Finset (Fin n)} (hf : MomentumIndep f) (hfS : PositionSupport f S) (hgT : MomentumSupport g T) (hST : Disjoint S T) (z : Chart n) : poissonBracket f g z = 0

★ Disjoint supports ⇒ vanishing bracket. The faithful form of the joint-arena argument: f (a control weight) is momentum-free and depends on positions in S; g (the interaction scalar) carries momentum dependence only on T; S and T disjoint. In the corpus S is the base — moment coordinates and the register angle — and T is the pointer, so the hypothesis is exactly the product structure of the arena. Note g is not assumed momentum-free: 𝓗 = Σⱼ wⱼ(x)hⱼ(q) is not.

theorem CSD.SigmaLayer.poissonBracket_comm_of_momentumIndep {n : ℕ} {f g : Chart n → ℝ} (hf : MomentumIndep f) (hg : MomentumIndep g) (z : Chart n) : poissonBracket f g z = 0

Two momentum-free functions always commute — the case {wᵢ, wⱼ} = 0, which needs no support hypothesis at all.

★ Conservation along the flow

noncomputable def CSD.SigmaLayer.hamiltonianField {n : ℕ} (H : Chart n → ℝ) (z : Chart n) : Chart n

The Hamiltonian vector field in canonical coordinates, X_H = (∂_y H, −∂_x H). No ω⁻¹ is needed: in a Darboux chart the inverse is the explicit swap-and-negate.

Equations

• CSD.SigmaLayer.hamiltonianField H z = (fun (i : Fin n) => CSD.SigmaLayer.dMom H z i, fun (i : Fin n) => -CSD.SigmaLayer.dPos H z i)

def CSD.SigmaLayer.BracketIsDerivative {n : ℕ} (f H : Chart n → ℝ) : Prop

The derivative of f along the Hamiltonian field is the bracket — the identity that turns "vanishing bracket" into "conserved". Stated as the hypothesis it is used through: f's derivative at z applied to X_H z is {f, H} z.

Equations

• CSD.SigmaLayer.BracketIsDerivative f H = ∀ (z : CSD.SigmaLayer.Chart n), (fderiv ℝ f z) (CSD.SigmaLayer.hamiltonianField H z) = CSD.SigmaLayer.poissonBracket f H z

theorem CSD.SigmaLayer.conserved_of_bracket_eq_zero {n : ℕ} {f H : Chart n → ℝ} (hd : BracketIsDerivative f H) (hzero : ∀ (z : Chart n), poissonBracket f H z = 0) {γ : ℝ → Chart n} (hγ : ∀ (t : ℝ), HasDerivAt γ (hamiltonianField H (γ t)) t) (hf : ∀ (t : ℝ), DifferentiableAt ℝ f (γ t)) (t : ℝ) : HasDerivAt (fun (s : ℝ) => f (γ s)) 0 t

★ Vanishing bracket ⇒ conserved along any integral curve. The conclusion the joint-arena route needs: if {f, H} = 0 then f is constant along the flow of H, so a control weight with vanishing bracket is a constant of motion even though the conjugate variables move. (BracketIsDerivative is the chain-rule step, taken as a hypothesis so this theorem is about the dynamics and not about differentiability bookkeeping.)

theorem CSD.SigmaLayer.weight_conserved_of_disjoint {n : ℕ} {w H : Chart n → ℝ} {S T : Finset (Fin n)} (hw : MomentumIndep w) (hwS : PositionSupport w S) (hHT : MomentumSupport H T) (hST : Disjoint S T) (hd : BracketIsDerivative w H) {γ : ℝ → Chart n} (hγ : ∀ (t : ℝ), HasDerivAt γ (hamiltonianField H (γ t)) t) (hf : ∀ (t : ℝ), DifferentiableAt ℝ w (γ t)) (t : ℝ) : HasDerivAt (fun (s : ℝ) => w (γ s)) 0 t

The weights are constants of motion: the packaged form of the two results above, in the shape BACKLOG.md A2 uses them — momentum-free control functions, an interaction scalar whose momentum dependence is disjoint from their position support.

★ The Koopman generator is the Liouvillian

theorem CSD.SigmaLayer.hasDerivAt_koopmanFun_poissonBracket {n : ℕ} {f H : Chart n → ℝ} (hd : BracketIsDerivative f H) {φ : ℝ → Chart n → Chart n} {x : Chart n} {t : ℝ} (hφ : HasDerivAt (fun (s : ℝ) => φ s x) (hamiltonianField H (φ t x)) t) (hf : DifferentiableAt ℝ f (φ t x)) : HasDerivAt (fun (s : ℝ) => Koopman.koopmanFun (φ s) f x) (poissonBracket f H (φ t x)) t

★ The Koopman generator is the Liouvillian. Along the Hamiltonian flow, the Koopman evolution of an observable differentiates to its Poisson bracket with H: the abstract generator of Mathlib/Dynamics/Koopman.lean (hasDerivAt_koopmanFun, the derivative of f along the flow's velocity field) read in a Darboux chart, where the velocity field is hamiltonianField H and the derivative along it is {f, H} (BracketIsDerivative, the chain-rule step taken as a hypothesis as everywhere else in this file). This is BACKLOG #47's Liouvillian half: the classical unitary group of Koopman–von Neumann has i{H, ·} as its generator on differentiable observables.