KineticNormalizedCanonicalMom
plain-language theorem explainer
A structure classifying CanonicalMom HKT targets whose kinetic sector is ultralocal-intensive: the momentum partial of the local Hamiltonian equals $2 c_{\mathrm{Kin}} p$ with nonzero scale, and the profile is $C^2$. Gravity/HKT workers cite it when restricting to kinetic-normalized dynamics before FTC recovery. Pure interface definition: bundles a repaired CanonicalMom target with the intensivity and smoothness witness; no proof content.
Claim. A kinetic-normalized CanonicalMom target consists of a point-split HKT target with canonical momentum density, together with a local Hamiltonian profile $h:\mathbb{R}^3\to\mathbb{R}$ that is $C^2$, and a nonzero constant $c_{\mathrm{Kin}}$, such that on the two-site phase space the Hamiltonian density equals $h(q_j,q_{j+1},\pi_j)$ and the momentum partial of $h$ satisfies $\partial_p h(a,b,p)=2 c_{\mathrm{Kin}}\,p$ for all configuration and momentum arguments.
background
Module setting is Wave C4/C5 gap5: after the mod-vacuum kill, the remaining half is kinetic-normalized rigidity. The ambient target is the repaired CanonicalMom class: local cells of the form $h(q_j,q_{j+1},\pi_j)$, a structure profile $g(q_j)$, and canonical momentum density $m_j=c_{\mathrm{Mom}}\pi_{j+1}(q_{j+1}-q_j)$ with $c_{\mathrm{Mom}}\neq 0$.
Phase space is the product of configuration and conjugate momentum on the periodic two-site lattice. A local Hamiltonian profile is any map $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$; smoothness packages its three partials (including the momentum response $h_p$) with a Fréchet-derivative cell identity. The profile map simply rewrites $h$ as a function on $\mathbb{R}\times\mathbb{R}\times\mathbb{R}$ so that $C^2$ can be stated in Mathlib form.
Intensivity here means the momentum partial is linear in $p$ alone: $h_p=2 c_{\mathrm{Kin}} p$. That is the kinetic-sector ultralocal normalization; the former assumed FTC-recovery field is no longer part of the class.
proof idea
No proof: this is a structure definition. It packages a CanonicalMom target with an existential witness (local profile $h$, smoothness data $S$, scale $c_{\mathrm{Kin}}$) asserting $C^2$ of the profile map, $c_{\mathrm{Kin}}\neq 0$, cellwise agreement of Hamiltonian density with $h$, and the intensivity identity $S.h_p(a,b,p)=(2 c_{\mathrm{Kin}})p$. Downstream theorems (notably FTC recovery) consume inhabitants of this type.
why it matters
Terminal interface for the kinetic half of gap5. The module doc records that FTC recovery is theorem-derived as ftc_recovery_of_normalized rather than an assumed class field; that theorem takes exactly this structure as input and rebuilds the full FTC package (profile, structure factor, canonical momentum scale) from intensivity plus $C^2$ plus the CanonicalMom functional equation.
Downstream, the same class feeds the universal-kinetic, quad-cost, calibrated-jet, and RCL-kinetic specializations in the recognition-cost kinetic module. In particular the ADM anchor still inhabits the weakened universal-kinetic class via conversion from a kinetic-normalized inhabitant, so the section has not emptied the target. Gap5 constraint-recovery flip is owned by the status ledger once both mod-vacuum and kinetic-normalized halves bind green (D-gap5-acceptance-adjudication-20260723).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.