hasDerivAt_hp_of_normalized
plain-language theorem explainer
Under C² smoothness of a local Hamiltonian density in the three phase-space slots, the momentum partial recorded by any LocalHamSmooth witness is the ordinary real derivative of the density in the momentum argument. Kinetic-from-cost theorems cite this to convert structural identities on the witness field into genuine one-variable calculus statements. The proof is a two-line rewrite: Frechet uniqueness of the profile map derivative, then equality of the witness slot with that Frechet directional derivative.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile and let $S$ be a $C^1$ cell-derivative witness for $h$, with $S_p$ the recorded momentum partial. If the packaged map $(a,b,p)\mapsto h(a,b,p)$ is $C^2$, then for every $(a,b,p)\in\mathbb{R}^3$ one has $\mathrm{HasDerivAt}\,\bigl(t\mapsto h(a,b,t),\, S_p(a,b,p),\, p\bigr)$.
background
The ambient module closes Wave C4/C5 gap5: after the mod-vacuum kill, the remaining work is kinetic-normalized rigidity for Hamilton–Jacobi–type local densities on a two-cell phase space. A local Hamiltonian profile is simply a real function $h(a,b,p)$ of two field values and one momentum. The structure LocalHamSmooth packages three partial-profile fields $(h_a,h_b,h_p)$ together with a cellwise Frechet derivative axiom that ties those fields to the actual differential of $h$ on each cell.
The packaging map sends $(a,b,p)$ to $h(a,b,p)$ on $\mathbb{R}^3$. ContDiff of order 2 on that map is the standing regularity hypothesis throughout the kinetic-normalized development; it supplies ordinary differentiability in each slot and uniqueness of Frechet derivatives. Upstream, hasDerivAt_profileMap_p already identifies the ordinary $p$-derivative of $h(a,b,\cdot)$ with the Frechet directional derivative of the packaging map along $(0,0,1)$. A companion uniqueness lemma equates the witness slot $S_p$ with that same directional derivative, independently of which smooth witness is chosen.
proof idea
Term-mode, two steps. First invoke the private lemma that, under ContDiff order 2 of the packaging map, the slice $t\mapsto h(a,b,t)$ has derivative equal to the Frechet directional derivative of the packaging map at $(a,b,p)$ in the direction $(0,0,1)$. Second, rewrite that directional derivative by the private equality identifying the LocalHamSmooth momentum slot $S_p(a,b,p)$ with the same Frechet value. The rewrite-with-assumption tactic finishes the goal. No new analysis is performed here; the theorem only transports the already-proved Frechet identification onto the ordinary one-variable derivative predicate.
why it matters
Every kinetic-from-recognition-cost identity that names an explicit formula for the momentum response needs this bridge. Downstream parents include costKinetic_hp_eq_sinh (response $w\kappa\sinh(\kappa p)$ from $J_{\log}=\cosh-1$), quadCost_hp_eq_linear and rclKinetic_hp_eq_linear (field-independent linear response from balance-jet and from the Recognition Composition Law), calibratedJet_hp_eq_linear, and the channel-separation pair universal_of_channelSeparated / channelSeparated_of_universal. The same fact feeds kinetic_split_of_intensivity inside the present module.
In the Recognition framework this is the calculus hinge that turns the T5 $J$-cost (and its RCL consequences) into a concrete kinetic term on the local Hamiltonian density, without treating the momentum partial as an extra axiom. Gap5's FTC recovery path (ftc_recovery_of_normalized) and the later constraint-close status both rely on having $S_p$ be a genuine derivative rather than a free field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.