hamDynLocalSmooth
plain-language theorem explainer
Packages Fréchet derivative data for the honest local Hamiltonian density on the two-site phase space, certifying that the quadratic kinetic-plus-structure profile is C¹ with explicit partials. Gravity rigidity proofs cite it when inhabiting the repaired CanonicalMom point-split target and when discharging PDE side conditions (constant kinetic slope, p-linearity). Construction is a pure structure fill: three partial profiles plus the cellwise derivative lemma.
Claim. The local Hamiltonian density $h(a,b,p)=\frac12\bigl(p^{2}+(1+a^{2})(b-a)^{2}\bigr)$ is $C^{1}$ on the two-site phase space: its partial profiles are $h_{a}=a(b-a)^{2}-(1+a^{2})(b-a)$, $h_{b}=(1+a^{2})(b-a)$, $h_{p}=p$, and for every cell index $j\in\mathbb{Z}/2\mathbb{Z}$ the Fréchet derivative of the cell map equals $h_{a}\,dq_{j}+h_{b}\,dq_{j+1}+h_{p}\,dp_{j}$.
background
Module setting is Wave C2 gap5: after the balanced-quartic falsifier kills strong point-split rigidity at $N=2$, the repaired class CanonicalMom asks for an honest Hamiltonian dynamics with a local density, a structure factor $g(q)=1+q^{2}$, and smooth cell data. No ledger flag is flipped.
A local Hamiltonian profile is a real function $h(a,b,p)$ of adjacent configuration values and the conjugate momentum. Smoothness is the structure that supplies three partial profiles $h_{a},h_{b},h_{p}$ together with a cellwise Fréchet certificate on the product phase space $(\mathbb{R}^{2}){q}\times(\mathbb{R}^{2}){p}$.
The honest density is $h=\frac12\bigl(p^{2}+(1+a^{2})(b-a)^{2}\bigr)$, written with the constant factor so Mathlib's product rule matches the recorded partials. Upstream, the three partials are defined pointwise and a lemma proves the cell derivative equals the corresponding linear combination of coordinate maps.
proof idea
Pure structure inhabitant, not a tactic proof. The four fields of the smoothness bundle are filled by name: partial in the first configuration slot, partial in the second, partial in momentum (which is simply the identity in $p$), and the already-proved cellwise HasFDerivAt lemma that expands the numerator by the product rule and scales by $1/2$. No further algebraic work occurs at this declaration.
why it matters
This is the smoothness witness for the honest HamDyn density inside the repaired CanonicalMom class. Downstream it is wired into the CanonicalMom point-split target itself, into scoped smooth rigidity data, and into the documentary PDE package: constant kinetic slope $1/2$, $h_{b}$ independent of $p$, $h_{p}$ linear in $p$, and the quadratic profile functional equation. Those lemmas are the Session-C route toward HKTRigidityStatementPointSplitDynN2Canonical under binding design D-qg-hkt-rigidity-route. In the broader SevenGaps gravity program it separates the physical kinetic-from-recognition-cost branch from the balanced-quartic counterexample that killed the stronger rigidity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.