ConstantKineticSlope
plain-language theorem explainer
Constant kinetic slope is the disclosed HKT kinetic-ultralocality gauge: the momentum partial of a smooth local Hamiltonian profile equals twice a fixed nonzero constant times p, independent of the configuration arguments. Gravity and CanonicalMom rigidity workers cite it to unlock conditional ADM quadratic recovery and hb gradient shape. It is a Prop definition packaging that conjunction, not a proved claim.
Claim. Let $h:\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be a local Hamiltonian profile with smooth partials $(h_a,h_b,h_p)$, and let $c_{\mathrm{kin}}\in\mathbb{R}$. The constant kinetic slope condition holds when $c_{\mathrm{kin}}\neq 0$ and $h_p(a,b,p)=2\,c_{\mathrm{kin}}\,p$ for all real $a,b,p$ (so $h$ integrates in $p$ to $c_{\mathrm{kin}}p^2$ plus a $p$-free remainder).
background
This module sits in Wave C2 gap5 of the CanonicalMom rigidity route. The local object is a profile $h:\mathbb{R}^3\to\mathbb{R}$ (arguments configuration pair $(a,b)$ and momentum $p$), packaged as LocalHamProfile. Smoothness is recorded by a structure supplying three partial profiles $h_a,h_b,h_p$ together with a cellwise Fréchet-derivative obligation on the two-point phase space.
The session finding is sharp: ContDiff-$\mathbb{R}$-2 of the profile does not by itself force the linear-$h_p$ / $p$-free-$h_b$ ansatz used by the PDE route. A smooth witness (square-root affine profile) satisfies the alternating functional equation yet has $p$-independent momentum partial and $b$-partial linear in $p$. The unconditioned quadratic solve therefore stays open; work proceeds under disclosed gauges.
Constant kinetic slope is exactly the kinetic half of those gauges: $h_p$ is forced to the ultralocal linear form $2 c_{\mathrm{kin}} p$ with $c_{\mathrm{kin}}\neq 0$, so integration in $p$ yields a pure $c_{\mathrm{kin}} p^2$ kinetic term.
proof idea
Pure Prop definition: the body is the conjunction $c_{\mathrm{kin}}\neq 0$ together with the pointwise identity that the momentum partial equals $(2 c_{\mathrm{kin}})\cdot p$ for every real triple $(a,b,p)$. No tactics, no lemmas, no reduction.
why it matters
This gauge is the kinetic half of the conditional ADM package. Downstream, ADM_quadratic_of_gauges takes constant kinetic slope plus FTC recovery from partials and returns the ADM quadratic form with $c_{\mathrm{Mom}}=4 c_{\mathrm{kin}} c_{\mathrm{Grad}}$. The companion hb_shape_of_constant_kinetic_slope specializes the alternating FE under this gauge (and $p$-independent $h_b$) to the gradient shape $h_b(a,b,0)=(c_{\mathrm{Mom}}/(2 c_{\mathrm{kin}})) g(a)(b-a)$.
The dynamical witness hamDyn_constantKineticSlope discharges the predicate at $c_{\mathrm{kin}}=1/2$ for the concrete HamDyn local profile. Both feed the smooth-scoped data package SmoothScopedCanonicalMomData (ContDiff-2 + linear ansatz + gauges) that lands the scoped rigidity theorem. In the gap5 ledger this is disclosed HKT kinetic ultralocality; it does not close the unconditioned solve_profile_FE_quadratic, and the module explicitly forbids flipping gap5_constraint_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.