vacuumShiftLocalHp
plain-language theorem explainer
The momentum partial of the vacuum-shift local Hamiltonian profile equals the HamDyn momentum partial: the added vacuum term a² is p-independent. Gravity and HKT-rigidity work cite it when assembling Fréchet derivatives and the LocalHamSmooth package for the n=2 vacuum-shift density. The definition is a one-line alias of the HamDyn p-slot.
Claim. Write $H_p$ for the partial of the local Hamiltonian density with respect to the momentum coordinate $p$. For the vacuum-shift profile $h(a,b,p)=\tfrac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)+a^2$, one has $H_p=H_p^{\mathrm{HamDyn}}$: the vacuum addend does not change the source-advection (momentum) slot of the local profile.
background
Module Wave C3 gap5 kills the unconditioned CanonicalMom rigidity statement by a vacuum-shift density at $n=2$. The density is
$$h(a,b,p)=\tfrac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)+a^2,$$
with structure factor $g(a)=1+a^2$ and CanonicalMom load $m_j=\pi_{j+1}(q_{j+1}-q_j)$. The ham–ham alternating functional equation is blind to the zero-gradient vacuum term $a^2$; the rigidity conclusion would force a constant vacuum while this density evaluates to $q^2$ on coincident configurations.
A LocalHamProfile packages the three partials of a local cell Hamiltonian in the $(a,b,p)$ chart (adjacent configuration coordinates and the momentum on the first site). The HamDyn profile already supplies those partials; the vacuum shift only adds $a^2$, which is independent of $p$. Hence the momentum partial is copied unchanged from HamDyn. Sibling aliases handle the $a$- and $b$-partials and the full profile.
proof idea
One-line definitional alias: the vacuum-shift momentum partial is definitionally equal to hamDynLocalHp, the corresponding HamDyn slot. No tactic proof; the mathematical content is that $\partial_p(a^2)=0$, so source advection is untouched by the vacuum sector.
why it matters
Feeds the vacuum-sector kill package for gap5. Downstream, hasFDerivAt_vacuumShiftLocalCell builds the Fréchet derivative of the local cell map as the linear combination of coordinate functionals weighted by the three partials, with this declaration as the $p$-weight. vacuumShiftLocalCellD_eq_profilePartials identifies the cell differential with those same weighted coordinates (starting from the HamDyn identity and adding the vacuum Fréchet term). vacuumShiftLocalSmooth packages the three partials into a LocalHamSmooth instance for the vacuum-shift profile.
In the Recognition gravity ledger this is the concrete witness that the vacuum sector leaves the momentum channel of the local Hamiltonian fixed while spoiling unconditioned CanonicalMom rigidity. The repaired terminal is the vacuum-modulo statement; whether structure-nonconstant plus the FE still forces the kinetic/gradient sectors remains open. Does not flip gap5 constraint recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.