kinetic_split_of_intensivity
plain-language theorem explainer
Under intensivity (momentum derivative linear in p) and C² smoothness of a local Hamiltonian profile, the profile splits as a pure quadratic kinetic term plus a p-independent remainder. Gravity/HKT rigidity arguments cite this to recover the kinetic shape before FTC reconstruction. The proof builds an auxiliary F with vanishing derivative and invokes constancy of differentiable zero-derivative maps.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile that is $C^2$ as a map on $\mathbb{R}\times\mathbb{R}\times\mathbb{R}$, and let $S$ be a smoothness package for $h$ whose momentum partial satisfies $\partial_p h(a,b,p)=(2c_{\mathrm{Kin}})p$ for a fixed real $c_{\mathrm{Kin}}$ and all $a,b,p$. Then for every $a,b,p\in\mathbb{R}$, $$h(a,b,p)=c_{\mathrm{Kin}}\,p^2+h(a,b,0).$$
background
This module closes the kinetic-normalized half of the HKT gap-5 ledger: after killing mod-vacuum rigidity by a variable-kinetic CanonicalMom counterexample, one works inside the intensivity field of KineticNormalizedCanonicalMom, where the momentum response of the local Hamiltonian density is forced to be linear in $p$.
A local Hamiltonian profile $h(a,b,p)$ is a real ternary function of adjacent configuration values and a conjugate momentum. The smoothness package supplies the partial $\partial_p h$ (written $S.hp$), and profileMap packages $h$ as a map $\mathbb{R}^3\to\mathbb{R}$ so that Mathlib $C^2$ and derivative lemmas apply. Intensivity here means exactly $\partial_p h(a,b,p)=(2c_{\mathrm{Kin}})p$ pointwise.
Upstream, hasDerivAt_hp_of_normalized converts the ContDiff-2 hypothesis into a genuine HasDerivAt statement for $t\mapsto h(a,b,t)$ with derivative $S.hp,a,b,t$. That is the only analytic input beyond the algebraic intensivity identity.
proof idea
Fix $a,b$ and define $F(t):=h(a,b,t)-c_{\mathrm{Kin}}t^2$. Differentiating: hasDerivAt_hp_of_normalized gives $\mathrm{HasDerivAt},h, (S.hp,a,b,t),t$; the power rule plus constant multiplication gives $\mathrm{HasDerivAt},(c_{\mathrm{Kin}}t^2),((2c_{\mathrm{Kin}})t),t$. Subtracting and rewriting $t\cdot t$ as $t^2$ yields $\mathrm{HasDerivAt},F,(S.hp,a,b,t-(2c_{\mathrm{Kin}})t),t$. Intensivity collapses the derivative to $0$.
Thus $F$ is differentiable with derivative identically zero, so is_const_of_deriv_eq_zero equates $F(p)$ and $F(0)$. Unwinding $F$ and rearranging by linarith produces $h(a,b,p)=c_{\mathrm{Kin}}p^2+h(a,b,0)$.
why it matters
This is the algebraic-analytic split that turns the intensivity field into an explicit quadratic kinetic term. Downstream, ftc_recovery_of_normalized packages FTC recovery as a derived theorem (not an assumed class field): from intensivity, ContDiff-2, and the CanonicalMom functional equation it extracts $h$, $c_{\mathrm{Kin}}$, a configuration potential $g$, and a nonzero momentum scale, with Hamiltonian density matching $h$ on phase space. The status flag theorem then records ftcRecoveryDerived and gap5_constraint_recovery as true once both ledger halves bind green.
In the Recognition gravity stack this is the kinetic half of gap-5 closure for HKT-style local Hamiltonians: after the mod-vacuum kill, normalized intensivity forces the $p^2$ shape that the eight-tick / CanonicalMom side needs before constraint recovery. It does not itself invoke the T5–T8 forcing chain, but it is the local PDE/FE step that makes kinetic normalization rigid enough for the gap-5 adjudication binding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.