vacuumKineticLocalProfile_contDiff2
plain-language theorem explainer
The vacuum kinetic local Hamiltonian profile is twice continuously Fréchet differentiable as a map from phase space R³ into R. Gap-closure work that isolates momentum derivatives of the Hamilton–Jacobi functional equation cites this smoothness certificate before any ∂/∂r step. The proof is a one-line term wrapper re-exporting the already-proved ContDiff result for that profile map.
Claim. The vacuum kinetic local Hamiltonian profile $h(a,b,p)=A(a)\,p^{2}+W(a,b)$ satisfies $\mathrm{ContDiff}\,\mathbb{R}\,2$ as a map $\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, thereby discharging the C2 strengthening obligation on local Hamiltonian profiles.
background
In the SevenGaps gravity stack, a local Hamiltonian profile is a smooth real function $h(a,b,p)$ of two configuration slots and one momentum slot. The vacuum kinetic profile is the concrete choice $h(a,b,p)=A(a),p^{2}+W(a,b)$, with $A$ a positive amplitude depending only on $a$ and $W$ a configuration coupling independent of $p$.
The ambient module closes Wave C4/C5 gap5: a mod-vacuum kill paired with kinetic-normalized CanonicalMom rigidity. Part of that program needs to differentiate the functional equation in the momentum coordinate $r$. The plain LocalHamSmooth package only identifies Fréchet coefficients of $h\circ\mathrm{coords}$; it does not license differentiability of those coefficient maps on $\mathbb{R}$.
Upstream, the C2 strengthening obligation therefore demands $\mathrm{ContDiff},\mathbb{R},2$ of the profile as a map $\mathbb{R}^{3}\to\mathbb{R}$ (or an equivalent slotwise HasDerivAt package) before any $\partial/\partial r$ isolation. A sibling theorem already proves that ContDiff statement for the vacuum kinetic profile map.
proof idea
One-line term wrapper. The obligation is definitionally ContDiff of the curried profile map on $\mathbb{R}\times\mathbb{R}\times\mathbb{R}$. The proof simply applies the sibling theorem that already establishes $\mathrm{ContDiff},\mathbb{R},2$ for that map (via rewriting the profile as $A(a)p^{2}+W(a,b)$ and invoking standard product and composition rules for ContDiff).
why it matters
This certificate is the missing smoothness gate for the algebraic PDE core of kinetic-normalized CanonicalMom rigidity: under a linear-$h_p$ / momentum-independent-$h_b$ ansatz, the functional equation forces the gradient coupling $h_b(a,b)\cdot\mathrm{kinCoeff}(b,a)=c_{\mathrm{Mom}}\cdot(b-a)\cdot g(a)$. Without ContDiff 2 on the profile, differentiating in the momentum slot is unlicensed.
The module binds the C5 upgrade of gap5 (mod-vacuum kill plus kinetic-normalized rigidity terminal). FTC recovery of the normalized intensivity field is theorem-derived rather than assumed as a class field; this smoothness fact sits on the kinetic half of that ledger. No downstream consumers are wired yet, but any later $\partial/\partial r$ isolation or gap5 constraint-recovery flip will need exactly this obligation discharged for the vacuum kinetic inhabitant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.