MomDynD
plain-language theorem explainer
Fréchet derivative of the two-site smeared momentum density, returned as a continuous linear map on phase space. Cited by the HasFDerivAt witness for that density and by the four partial-derivative evaluations that feed the point-split HKT bracket. Body is the product-rule expansion in the exact order Mathlib's HasFDerivAt.mul expects.
Claim. For a weight profile $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and a phase-space point $x=(q,\pi)\in(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})^2$, define the continuous linear map $D_x M_w:T_x\mathrm{PhaseSpace}_2\to\mathbb{R}$ by $$D_x M_w=(q_1-q_0)\cdot(w_0\,d\pi_1-w_1\,d\pi_0)+(w_0\pi_1-w_1\pi_0)\cdot(dq_1-dq_0).$$ This is the candidate Fréchet derivative of the point-split momentum functional $M_w(q,\pi)=(q_1-q_0)(w_0\pi_1-w_1\pi_0)$.
background
Phase space on the two-site periodic lattice is the product $(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. The continuous linear functionals $\mathrm{coordQ},i$ and $\mathrm{coordP},i$ extract the configuration and momentum coordinates $q_i$ and $\pi_i$ respectively.
The ambient module repairs the Hojman–Kuchař–Teitelboim dynamic target after the unsplit momentum–Hamiltonian field proved uninhabitable for nearest-neighbour profiles against a frozen quadratic Hamiltonian (singular when $p_0+p_1=0$). On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the generator-symmetric deformation vanishes identically; the repair therefore uses the smeared point-split momentum density already present in the Hamiltonian bracket identities, with source/target advection densities.
The doc-comment fixes the product-rule order to match Mathlib: $f(x)\cdot g'+g(x)\cdot f'$. Here $f=q_1-q_0$ and $g=w_0\pi_1-w_1\pi_0$, so the two summands of this definition are exactly those factors.
proof idea
Pure definition: no tactics. The body is the sum of two scalar multiplications of continuous linear maps, $(q_1-q_0)\bullet(w_0,\mathrm{coordP},1-w_1,\mathrm{coordP},0)$ plus $(w_0\pi_1-w_1\pi_0)\bullet(\mathrm{coordQ},1-\mathrm{coordQ},0)$, which is the product-rule expansion of $M_w$ evaluated at the base point $x$. Downstream lemmas simply rewrite with this definition after invoking the Fréchet-derivative witness.
why it matters
Load-bearing derivative object for the point-split HKT dynamic target. The lemma hasFDerivAt_MomDyn asserts that this map is the genuine Fréchet derivative of the smeared momentum density; the four theorems pderivP_MomDyn_zero/one and pderivQ_MomDyn_zero/one then read off the coordinate partials by applying the map and simplifying.
Those partials are the concrete inputs to the momentum sector of the strong point-split target class. Module scope is deliberately narrow: no rigidity theorem, no ledger flag flip. The unsplit Dyn target remains as the falsification-adjacent record; this definition is part of the repaired sibling that makes the momentum–Hamiltonian bracket inhabitably smooth at $n=2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.