The Jacobi identity for the Lie–Poisson bracket on the regular dual of sdiff(T^3), with every cancellation displayed

Expository note (version 1.1). We give a self-contained derivation of the Jacobi identity for the Lie–Poisson bracket {F,G}(m) = ⟨m, [δF/δm, δG/δm]⟩ on the regular dual of the Lie algebra sdiff(T^3) of smooth divergence-free vector fields on the flat torus. We compute the functional derivative δ{G,H}/δm = [g,h] + Hess_G(m)(K_h m) − Hess_H(m)(K_g m) exactly, expand the cyclic sum completely, display all six second-derivative terms and show that they cancel in three pairs by the symmetry of second derivatives, leaving ⟨m, vector-field Jacobiator⟩ = 0. The vector-field Jacobi identity is proved by writing out all twelve terms. We also derive the vorticity form, explain the role of the constant (harmonic) fields, and correct an integration-by-parts step of an earlier informal draft by an explicit counterexample. Classical, not new. This is a classical theorem (Arnold 1966; Marsden–Weinstein 1983). The note claims no new result and makes no claim about the Euler or Navier–Stokes equations, about any symmetric (metriplectic, "tether") term, or about finite-Fourier models. What Lean checks. Only the final algebraic cancellation (Steps 4–5): LiePoissonCore.six_terms_cancel and LiePoissonCore.lie_poisson_jacobi_core in FTVerified/Companion/LiePoissonJacobiCore.lean, for an arbitrary Lie algebra over a commutative ring, a linear m and symmetric Q_F, Q_G, Q_H (axioms: propext, Quot.sound). Pen and paper only (written out in the note): the symmetry of second derivatives, the product lemma, the formula for δ{G,H}/δm, the torus, the Leray projection and the admissible function class. The attached sympy and exact-quadrature checks were re-run on 11 November 2026 at the pinned commit and reproduce the committed outputs exactly (ALL PASS); they are evidence, not proofs. Hypothesis-to-assumption table (README.md): m linear = the pairing with the state; Q symmetric = the symmetry-of-second-derivatives lemma; [LieRing L] [LieAlgebra R L] = the vector-field Lie algebra, whose Jacobi identity the note proves separately. No mismatch was found. Reproducibility. Full Lean source: BenFrohman/frohmanian-tether-verified at a761aed99fba58ed4ac9bd5970577b2fc089824d (tip of main on 11 November 2026; a git archive zip of that commit is attached). The paper cites code commit cf04afd; the Lean sources, scripts, lakefile, manifest and toolchain are byte-identical between that commit and a761aed. Lean leanprover/lean4:v4.30.0-rc1, Mathlib 0c154d67103f74be3a0f2c509f72ccbf5be9f2a7. One-command rebuild from the repository root: lake exe cache get && lake build && python3 scripts/check_jacobi_axioms.py. GitHub Actions on main at a761aed passed (run 42932429909). On 11 November 2026 the pinned commit was rebuilt locally from scratch for the project modules (attached build.log); the attached axiom output (axiom-output.txt: PASS, 49 declarations) shows only propext, Classical.choice and Quot.sound (or a subset), and the attached scan found no sorry, admit, native_decide or axiom declarations. SHA256SUMS lists every attached file. Limits. A kernel check shows that the stated Lean propositions follow from the stated Lean definitions. It does not show that those definitions model any geometric or physical object.