hasFDerivAt_MomDyn
plain-language theorem explainer
The smeared point-split momentum functional MomDyn(w) on the n=2 phase space is Fréchet differentiable at every point, with derivative the continuous linear map MomDynD(w,x) built from the product rule. Anyone assembling HKT point-split Poisson brackets or partials of the momentum sector cites this. The proof rewrites MomDyn as a product of two coordinate differences via the closed form, then chains coordinate Fréchet derivatives under subtraction and multiplication.
Claim. For every weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and every phase-space point $x\in T^*\mathbb{R}^{\mathbb{Z}/2\mathbb{Z}}$, the map $y\mapsto \mathrm{MomDyn}(w)(y)$ is Fréchet differentiable at $x$ with derivative equal to the continuous linear map $\mathrm{MomDynD}(w,x)$ given by the product rule on $(q_1-q_0)\cdot(w_0 p_1-w_1 p_0)$.
background
This module repairs the Hojman–Kuchař–Teitelboim dynamic target after the unsplit momentum–Hamiltonian field proved uninhabitable for honest nearest-neighbor profiles against the frozen quadratic Hamiltonian at $n=2$. The load-bearing object is the strong point-split target; the momentum sector uses a smeared point-split density rather than an unsplit advection term.
On phase space $\mathrm{PhaseSpace},2=(q,p)$ with coordinates indexed by $\mathbb{Z}/2\mathbb{Z}$, the smeared momentum is $\mathrm{MomDyn}(w)(x)=\sum_j w_j,\mathrm{momDynDensity}(x,j)$. The closed identity $\mathrm{MomDyn_closed}$ collapses the sum to the bilinear form $(q_1-q_0)(w_0 p_1-w_1 p_0)$. The candidate derivative $\mathrm{MomDynD}$ is exactly the product-rule linear map $f(x),g'+g(x),f'$ for those two factors.
Upstream coordinate lemmas $\mathrm{hasFDerivAt_coord_fst}$ and $\mathrm{hasFDerivAt_coord_snd}$ supply Fréchet derivatives of the individual $q_j$ and $p_j$ projections on this finite-dimensional phase space.
proof idea
First prove a functional equality: $\mathrm{MomDyn}(w)$ equals the pointwise product $((y\mapsto y.1,1)-(y\mapsto y.1,0))\cdot((y\mapsto w_0,y.2,1)-(y\mapsto w_1,y.2,0))$, by funext and MomDyn_closed after unfolding the $\Pi$-subtraction. Rewrite the goal along that identity. The remainder is a one-shot chain: Fréchet derivative of $q_1$ minus that of $q_0$, times (constant-multiple of $p_1$ minus constant-multiple of $p_0$), using hasFDerivAt_coord_fst, hasFDerivAt_coord_snd, .sub, .const_mul, and .mul. The resulting linear map matches the definition of $\mathrm{MomDynD}$.
why it matters
Differentiability of the point-split momentum is the analytic gate for the strong HKT point-split target on $n=2$. Downstream, differentiable_MomDyn is the global Differentiable wrapper, and the four partials pderivQ_MomDyn_zero/one and pderivP_MomDyn_zero/one read off the components of $\mathrm{MomDynD}$ needed for Poisson brackets and the non-abelian $\mathrm{mom_mom}$ Wronskian density noted in the module header.
In the SevenGaps gravity campaign this sits inside the Wave C2 R5 repair: unsplit $\mathrm{mom_ham}$ is singular on $p_0+p_1=0$, so the framework switches to smeared source/target advection densities. No rigidity theorem and no ledger flag are claimed here; the lemma only certifies that the repaired momentum functional is $C^1$ so bracket identities can be stated honestly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.