hasDerivAt_profileMap_p
plain-language theorem explainer
If a local Hamiltonian density is C² as a map on (a,b,p)-space, its ordinary partial in the momentum slot equals the Fréchet derivative of the packaged profile map applied to (0,0,1). Cited when recovering LocalHamSmooth momentum coefficients from ContDiff data. Proof is chain rule along the affine line t ↦ (a,b,t).
Claim. Let $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ be a local Hamiltonian profile, and write $\Phi_h(a,b,p)=h(a,b,p)$. If $\Phi_h$ is $C^2$, then for all $a,b,p\in\mathbb{R}$ the map $t\mapsto h(a,b,t)$ is differentiable at $p$ with derivative $D\Phi_h(a,b,p)\cdot(0,0,1)$.
background
The module closes Wave C4/C5 gap5: after killing the mod-vacuum HKT rigidity claim, it builds kinetic-normalized CanonicalMom rigidity, with FTC recovery derived rather than assumed.
A LocalHamProfile is simply a real ternary map $h(a,b,p)$, the local Hamiltonian density in amplitude, weight, and momentum. The packaging profileMap turns it into $\Phi_h:\mathbb{R}^3\to\mathbb{R}$, $\Phi_h(a,b,p)=h(a,b,p)$, so standard multivariable calculus applies.
ContDiff of order 2 on $\Phi_h$ supplies Fréchet derivatives along coordinate directions. The third slot is the momentum coordinate; its directional derivative is the object later matched to the hp coefficient of a LocalHamSmooth witness.
proof idea
From ContDiff order 2, drop to order 1 and extract hasFDerivAt of $\Phi_h$ at $(a,b,p)$. Separately, the affine path $\varphi(t)=(a,b,t)$ has ordinary derivative $(0,0,1)$ at $p$ by product of two constant derivatives and the identity. Chain rule (comp_hasDerivAt) yields a derivative for $\Phi_h\circ\varphi$. Unfolding profileMap and function composition identifies $\Phi_h\circ\varphi$ with $t\mapsto h(a,b,t)$, finishing the claim.
why it matters
Feeds hasDerivAt_hp_of_normalized, which rewrites the Fréchet directional derivative as the smooth-structure coefficient $S.hp$, so ContDiff-2 data alone recovers the momentum slot of LocalHamSmooth. That step is part of kinetic-normalized rigidity: intensivity and FTC recovery become theorems rather than class fields, supporting the gap5 constraint-close ledger after the mod-vacuum kill. In the broader SevenGaps gravity program this is calculus infrastructure, not a forcing-chain landmark, but it is required to make the normalized CanonicalMom PDE side fully theorem-derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.