hasDerivAt_profileMap_b
plain-language theorem explainer
Under C² regularity of a local Hamiltonian profile packaged as a map on R³, the ordinary derivative in the middle slot equals the Fréchet derivative applied to the unit vector (0,1,0). Gravity/HKT rigidity proofs cite it to identify partials of the kinetic-normalized density with directional derivatives. The argument is chain rule: ContDiff gives hasFDerivAt, composed with the affine line s ↦ (a,s,p).
Claim. Let $h:\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ be a local Hamiltonian profile and write $\Phi(a,b,p)=h(a,b,p)$. If $\Phi$ is $C^2$, then for all $a,b,p\in\mathbb{R}$ the map $s\mapsto h(a,s,p)$ is differentiable at $b$ with derivative $D\Phi(a,b,p)\cdot(0,1,0)$.
background
The module closes Wave C4/C5 gap5 for HKT: after killing the mod-vacuum rigidity claim, it develops kinetic-normalized CanonicalMom rigidity, with FTC recovery proved rather than assumed as a class field.
A LocalHamProfile is simply a real ternary function $h(a,b,p)$, the local Hamiltonian density in the three canonical coordinates. profileMap repackages it as $\Phi:\mathbb{R}^3\to\mathbb{R}$, $\Phi(t)=h(t_1,t_2,t_3)$, so multivariable calculus (Fréchet derivatives, ContDiff) applies directly.
The middle coordinate $b$ is the slot whose partial must match the intensivity field hb of a smooth local Hamiltonian structure. This lemma is the pure calculus bridge between that partial and $D\Phi\cdot(0,1,0)$.
proof idea
From ContDiff of order 2, drop to order 1 and extract hasFDerivAt of $\Phi$ at $(a,b,p)$. Separately, the affine path $\varphi(s)=(a,s,p)$ has derivative $(0,1,0)$ at $b$ by product of constant and identity derivatives. Compose via comp_hasDerivAt to get a derivative for $\Phi\circ\varphi$. Unfold profileMap and Function.comp to identify $\Phi\circ\varphi$ with $s\mapsto h(a,s,p)$.
why it matters
Feeds hasDerivAt_hb_of_normalized, which rewrites the same derivative as the intensivity field $S.hb$ of a LocalHamSmooth structure. That identification is required for kinetic-normalized CanonicalMom rigidity: partials of the vacuum kinetic density must equal the design intensivity fields so FTC recovery can be theorem-derived rather than postulated.
In the SevenGaps gravity ledger this sits in the C5 half of gap5 (binding D-gap5-acceptance-adjudication-20260723). It is pure analysis scaffolding inside the HKT rigidity path, not a Recognition landmark (T0–T8, RCL, phi) itself, but it is load-bearing for the kinetic-normalized terminal that flips gap5_constraint_recovery once both ledger halves bind green.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.