hamDynLocalCellD
plain-language theorem explainer
Continuous linear map giving the Fréchet derivative of the local Hamiltonian density cell on the two-site phase space, at point x for site j. Gravity workers on the HKT canonical-momentum target cite it as the derivative witness for the honest HamDyn inhabitant. The body is an explicit product-rule expansion of the local numerator, scaled by 1/2, assembled from configuration and momentum coordinate functionals.
Claim. For each site $j \in \mathbb{Z}/2\mathbb{Z}$ and phase-space point $x=(q,\pi)\in (\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$, the map $D_{j,x}:T_x\mathrm{PhaseSpace}_2\to\mathbb{R}$ is the continuous linear functional obtained by Mathlib's product-rule expansion of the local Hamiltonian numerator, scaled by $1/2$.
background
The ambient model is the canonical phase space of a lattice wave field: configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ and conjugate momentum $\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ on a periodic lattice with $n$ sites. Here $n=2$. The maps $\mathrm{coordQ}_i$ and $\mathrm{coordP}_i$ are the continuous linear functionals extracting $q_i$ and $\pi_i$ respectively (projections composed with the product factors).
This module is Wave C2 gap5 work on the HKT point-split target: Session B defines the canonical-momentum class, exhibits an honest HamDyn inhabitant, and banks a DEFINED-only rigidity statement for $N=2$. The local cell is the scalar profile of the Hamiltonian density at a single bond $(j,j+1)$, whose Fréchet data must match Mathlib's product-rule expansion so that HasFDerivAt proofs go through without ad-hoc calculus.
proof idea
Pure definition, not a proof. The body builds a continuous linear map by scaling the sum of three product-rule blocks by $1/2$: a doubled $\pi_j,\mathrm{coordP}j$ term; a factor $(1+q_j^2)$ times a doubled $(q{j+1}-q_j)(\mathrm{coordQ}_{j+1}-\mathrm{coordQ}j)$ term; and a factor $(q{j+1}-q_j)^2$ times a doubled $q_j,\mathrm{coordQ}_j$ term. Each block is written with the doubled sum form Mathlib's product rule emits, so the later HasFDerivAt lemma can match term-by-term.
why it matters
This is the derivative witness for the honest HamDyn local cell in the repaired CanonicalMom class (Session B of the gap5 binding design). Downstream, hamDynLocalCellD_eq_profilePartials rewrites it as the linear combination of $\mathrm{coordQ}j$, $\mathrm{coordQ}{j+1}$, and $\mathrm{coordP}_j$ with the three scalar partials of the local profile; hasFDerivAt_hamDynLocalCell_raw then certifies that this map is the true Fréchet derivative of that profile. The vacuum-sector kill path reuses it: vacuumShiftLocalCellD is this map plus a $2q_j,\mathrm{coordQ}_j$ correction, and the corresponding HasFDerivAt lemma reduces through the HamDyn derivative. No ledger flag is flipped; the object only supports the DEFINED-only canonical rigidity statement that later sessions aim to prove.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.