hasDerivAt_hb_of_normalized
plain-language theorem explainer
Under C² smoothness of a local Hamiltonian profile, the named partial S.hb is the ordinary derivative of h(a,·,p) at b. Kinetic-normalized rigidity proofs cite this to justify FTC along the b-line. The argument rewrites the directional fderiv of the packaged profile map into the LocalHamSmooth field hb.
Claim. Let $h$ be a local Hamiltonian profile with a $C^2$ smoothness witness $S$, and assume the packaged map $(a,b,p)\mapsto h(a,b,p)$ is $C^2$. Then for all real $a,b,p$, the map $s\mapsto h(a,s,p)$ is differentiable at $s=b$ with derivative equal to the partial field $S.h_b(a,b,p)$.
background
This module closes the kinetic-normalized half of the HKT gap-5 ledger: after killing the mod-vacuum rigidity claim, one works with an intensivity field on a local Hamiltonian density and recovers the kinetic split by calculus rather than by assuming an FTC class field.
A LocalHamProfile is a real ternary density $h(a,b,p)$. The helper profileMap packages it as a map $\mathbb{R}^3\to\mathbb{R}$. LocalHamSmooth supplies named partials $h_a,h_b,h_p$ meant to match those derivatives once $C^2$ is known. The private lemma hasDerivAt_profileMap_b already identifies the $b$-line derivative with the Fréchet derivative of profileMap in the direction $(0,1,0)$.
The companion identity LocalHamSmooth_hb_eq_fderiv equates the structure field $S.h_b$ with that same directional derivative. Together they turn the abstract partial into a genuine one-variable HasDerivAt fact usable by the fundamental theorem of calculus.
proof idea
Term-mode, two steps. First apply the private line lemma hasDerivAt_profileMap_b to obtain
HasDerivAt (fun s => h a s p) (fderiv (profileMap h) (a,b,p) (0,1,0)) b
from the $C^2$ hypothesis on profileMap. Then rewrite the derivative value by the equality LocalHamSmooth_hb_eq_fderiv, which replaces the directional Fréchet derivative by the named field $S.h_b(a,b,p)$. The rwa closes the goal.
why it matters
Feeds gradient_recovery_of_intensivity, the gradient-sector FTC that integrates the functional-equation-forced $h_b$ off the diagonal to recover intensivity structure. That parent is the calculus engine behind the kinetic split
$h(a,b,p)=c_{\mathrm{Kin}}p^2+h(a,b,0)$
stated in the module section header, and ultimately behind the theorem-derived (not assumed) FTC recovery ftc_recovery_of_normalized that the module doc flags as the C5 upgrade.
In the Seven Gaps gravity program this is bookkeeping that makes the kinetic-normalized CanonicalMom rigidity claim honest: partials used in the HKT local functional equation are actual derivatives, so integration along coordinate lines is justified. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those sit upstream in the T5–T8 chain. It only licenses the calculus step that turns intensivity plus $C^2$ into the normalized kinetic form used to close gap 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.