hamDynKineticNormalized
plain-language theorem explainer
Packages the honest HamDyn point-split target as a kinetic-normalized CanonicalMom inhabitant at n=2, with kinetic slope c_Kin = 1/2. Gravity and HKT-rigidity authors cite it as the concrete ADM anchor inside the kinetic-normalized class. The body is a structure instance: local profile, ContDiff-2, density match, and the intensivity identity h_p = p = 2 c_Kin p.
Claim. The honest HamDyn point-split target carries a kinetic-normalized CanonicalMom structure at $n=2$: there exist a local Hamiltonian profile $h$, smoothness data $S$, and $c_{\mathrm{Kin}}=1/2\neq 0$ such that the Hamiltonian density equals $h$ on phase space, the profile map is $C^2$, and the momentum partial satisfies $S.h_p(a,b,p)=(2c_{\mathrm{Kin}})p$ for all $a,b,p\in\mathbb{R}$.
background
Module Wave C4/C5 gap5 closes the kinetic-normalized half of the HKT mod-vacuum ledger. The intensivity field is the structure KineticNormalizedCanonicalMom: a CanonicalMom point-split target together with a witness that the local Hamiltonian profile is $C^2$ and ultralocally intensive in momentum, $h_p=2c_{\mathrm{Kin}}p$ with $c_{\mathrm{Kin}}\neq 0$. The former assumed FTC-recovery field is discharged separately as a theorem (ftc_recovery_of_normalized).
The honest HamDyn density is written through the local profile $h(a,b,p)=\tfrac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)$, so Frechet data match Mathlib's product rule. Its momentum partial is simply $h_p(a,b,p)=p$. Upstream lemmas already give ContDiff-2 of this profile, equality of the global density with the local profile, and the CanonicalMom point-split packaging of HamDyn.
proof idea
One structure instance. Set target to the existing HamDyn CanonicalMom point-split package. For the kinetic-normalized witness, refine with the HamDyn local profile, its smoothness bundle, and $c_{\mathrm{Kin}}=1/2$. Discharge ContDiff-2 by hamDynLocalProfile_contDiff2, non-vanishing by norm_num, and density match by hamDynDensity_eq_localProfile. The remaining intensivity goal is $h_p(a,b,p)=(2\cdot\tfrac12)p$; unfold $h_p\equiv p$ and finish by ring.
why it matters
Supplies the non-empty kinetic-normalized inhabitant that the terminal rigidity Prop quantifies over. Downstream, hamDyn_satisfies_kineticNormalized reads off the ADM quadratic form with $c_{\mathrm{Mom}}=4c_{\mathrm{Kin}}c_{\mathrm{Grad}}$ on this instance, and hamDynUniversalKinetic coerces it into the weakened universal-kinetic class so that class is not emptied by the gap5 kill. In the module ledger this is the green anchor for the kinetic-normalized half of gap5 (binding D-gap5-acceptance-adjudication-20260723), complementary to the mod-vacuum non-existence half. It does not itself run the full rigidity argument; that is HKTRigidityKineticNormalizedN2_holds via FTC recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.