hamDynSmoothScopedData
plain-language theorem explainer
Packages the honest HamDyn local Hamiltonian as smooth-scoped canonical-momentum rigidity data: ContDiff-2 profile, linear momentum partial, p-independent b-partial, kinetic slope 1/2, vacuum gauge 0, and structure factor g(q)=1+q². Downstream smooth-scoped HKT rigidity for the dynamical point-split target cites this instance. The body is a structure witness wiring already-proved component lemmas and algebraic checks.
Claim. The honest HamDyn local Hamiltonian profile, with its smoothness witness, structure factor $g(q)=1+q^2$, momentum coefficient $c_{\mathrm{Mom}}=1$, kinetic slope $c_{\mathrm{Kin}}=1/2$, and vacuum gauge $c_{\mathrm{Vac}}=0$, forms a complete smooth-scoped canonical-momentum data package for the dynamical point-split HKT target: ContDiff-$2$ of the local profile, the linear-$h_p$ / $p$-free-$h_b$ ansatz, constant kinetic and vacuum gauges, the alternating functional equation, and recovery of the profile from its partials.
background
Module setting is Wave C2 gap5: CanonicalMom rigidity under the ContDiff-2 smoothness hypothesis on the local Hamiltonian profile (as a map $\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$). ContDiff-2 is the standard HKT smoothness assumption; the module discloses that it does not by itself force the linear-$h_p$ / $p$-independent-$h_b$ ansatz used on the PDE route (the smooth counterexample sqrtAffineProfile satisfies the alternating FE yet violates that ansatz).
SmoothScopedCanonicalMomData is the data package that bundles a local Hamiltonian profile, its smoothness witness, a structure factor $g$, nonzero momentum coefficient, ContDiff-2 obligation, the linear ansatz, constant kinetic/vacuum gauges, the alternating FE, and recovery from partials. Honest HamDyn is the concrete dynamical density whose local profile is quadratic in the momentum coordinate with structure factor $1+q^2$.
Upstream component facts already established for this profile: ContDiff-2 of the profile map; $h_p$ linear in $p$ with unit slope; $h_b$ independent of $p$; constant kinetic slope $1/2$; constant vacuum gauge $0$; and equality of the dynamical density with the local profile.
proof idea
Definitional structure instance, not a tactic proof. The local profile and smoothness witness are set to the honest HamDyn pair; $g(q):=1+q^2$; coefficients $c_{\mathrm{Mom}}=1$, $c_{\mathrm{Kin}}=1/2$, $c_{\mathrm{Vac}}=0$ with $c_{\mathrm{Mom}}\neq 0$ by norm_num.
ContDiff-2 is discharged by hamDynLocalProfile_contDiff2. Density/structure/momentum profile equalities cite hamDynDensity_eq_localProfile, the structure-factor identity, and the canonical momentum density lemma. The alternating FE reduces by unfolding the local $h_b$/$h_p$ and a ring identity. Linear-$h_p$, $p$-free-$h_b$, constant kinetic slope, and constant vacuum gauge are the four named component theorems. Recovery from partials is a two-sided algebraic check (including the coefficient identity $1/(4\cdot(1/2))=1/2$).
why it matters
This is the honest HamDyn ContDiff-2 + ansatz discharge listed as landing item 5 of the gap5 session. It feeds hamDyn_smooth_scoped_rigidity, which extracts the ADM quadratic form
$c_{\mathrm{Kin}},p^2 + c_{\mathrm{Grad}},g,(\partial q)^2 + c_{\mathrm{Vac}}$
with the HKT relation $c_{\mathrm{Mom}}=4,c_{\mathrm{Kin}},c_{\mathrm{Grad}}$ for the dynamical point-split canonical-momentum target.
In the Recognition gravity stack this closes the smooth-scoped side of the HKT rigidity route under disclosed kinetic ultralocality and vacuum normalization, without claiming the unconditioned functional-equation solve. The module explicitly keeps solve_profile_FE_quadratic open and forbids flipping gap5_constraint_recovery: ContDiff-2 alone is not a forcing principle for the linear ansatz (credit-bearing scope correction via the sqrt-affine counterexample).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.