hamDyn_HpLinearInP
plain-language theorem explainer
For the honest HamDyn local density, the momentum partial is linear in p with kinetic coefficient identically 1. Cited when packaging HamDyn into smooth-scoped CanonicalMom rigidity data under the linear-hp ansatz. Proof is a direct existence witness: constant coefficient 1, then simp against the explicit hp field.
Claim. Let $h(a,b,p)=\frac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)$ be the honest local HamDyn profile, with its standard smooth structure $S$. Then the momentum partial is linear in $p$: there exists $k:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ such that $S.h_p(a,b,p)=k(a,b)\,p$ for all $a,b,p\in\mathbb{R}$.
background
Session C2 of the HKT CanonicalMom rigidity route works with local Hamiltonian profiles $h:\mathbb{R}^3\to\mathbb{R}$ in coordinates $(a,b,p)$, plus a smooth structure $S$ supplying partials $h_a$, $h_b$, $h_p$ and Fréchet cell data. The predicate "hp linear in p" means $\exists,k(a,b)$ with $S.h_p(a,b,p)=k(a,b),p$.
The module finding is that $\mathrm{ContDiff},\mathbb{R},2$ of the profile alone does not force this ansatz from the alternating functional equation: the smooth sqrt-affine witness satisfies the FE with $c_{\mathrm{Mom}}=1$, $g\equiv 1$, yet fails linear hp. The unconditioned quadratic FE solve therefore stays open.
The honest HamDyn density is $h=\frac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)$, with explicit momentum partial $h_p(a,b,p)=p$. This theorem records that this concrete profile does discharge the linear-hp obligation used by the PDE route under disclosed kinetic ultralocality.
proof idea
Short term proof. Exhibit the kinetic coefficient as the constant map $(a,b)\mapsto 1$. Introduce $a,b,p$ and simplify against the definitions of the HamDyn smooth structure and its momentum partial, which is definitionally the projection $(a,b,p)\mapsto p$. The identity $p=1\cdot p$ closes the goal.
why it matters
Feeds the packaging that supplies honest HamDyn as smooth-scoped CanonicalMom rigidity data (profile, smooth structure, gauge $g(q)=1+q^2$, $c_{\mathrm{Mom}}=1$). That packaging is the honest ContDiff-2 plus ansatz discharge listed in the module finding, and supports smooth-scoped rigidity for the point-split dynamical $N=2$ CanonicalMom target.
In the Recognition Science gravity SevenGaps / HKT route this is a concrete discharge for the physical HamDyn density, not a forcing theorem: ContDiff-2 does not force linear hp in general (counterexample already landed). It does not flip gap5_constraint_recovery; the unconditioned profile FE solve remains open. Downstream work that needs the linear-hp hypothesis on HamDyn cites this rather than re-deriving the coefficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.