hamDynLocalHa
plain-language theorem explainer
Explicit a-partial of the local Hamiltonian density used by the honest HamDyn inhabitant on two-site phase space. Gravity workers cite it when packaging cell Fréchet derivatives or building the vacuum-shifted profile. The body is a closed cubic polynomial in the neighboring configuration coordinates, ignoring momentum.
Claim. Define the first-configuration partial of the local Hamiltonian profile by $H_a(a,b,p) = a(b-a)^2 - (1+a^2)(b-a)$ for all real $a,b,p$. (The momentum slot is dummy.)
background
In the SevenGaps HKT stack, a local Hamiltonian profile is simply a real ternary map $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ giving the on-cell energy density from neighboring configuration values and the local momentum. The module repairs the CanonicalMom class after killing the strong point-split rigidity route (Wave C2 gap5): Session B exhibits an honest dynamical HamDyn inhabitant and banks a DEFINED-only rigidity statement for later sessions.
The three partials of that density (with respect to the two configuration slots and the momentum slot) are the building blocks of the cell Fréchet derivative on PhaseSpace 2. Upstream, LocalHamProfile is only the type alias; no further structure is imposed here. Downstream vacuum work reuses the same a-partial and adds a linear shift $2a$.
proof idea
Pure definition: the ternary map is written out as the polynomial $a(b-a)^2-(1+a^2)(b-a)$, with the third argument unused. No lemmas are invoked.
why it matters
This partial is the ha field of the local smoothness package for the honest HamDyn model, and it appears verbatim in the cell derivative identity that expands the Fréchet derivative as a linear combination of coordinate maps. The vacuum-sector kill module defines its shifted a-partial by adding $2a$ to this formula and reuses the same expansion pattern. Together these close the analytic side of the repaired CanonicalMom target without flipping the gap5 ledger flag. Framework-wise it is pure gravity scaffolding inside the HKT point-split program, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.