vacuumShiftLocalCellD
plain-language theorem explainer
Frechet data for the vacuum-shifted local Hamiltonian cell on the two-site lattice: HamDyn cell derivative plus the linear term from the vacuum smear q_j^{2}. Gravity/HKT auditors cite it when checking that the vacuum correction is differentiable and matches profile partials. The body is a one-line sum of continuous linear maps, not a proved identity.
Claim. For each site $j\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x=(q,\pi)$ on the two-site lattice, define the continuous linear map $D_j^{\mathrm{vac}}(x):\mathrm{PhaseSpace}_2\to\mathbb{R}$ by $D_j^{\mathrm{vac}}(x)=D_j^{\mathrm{HamDyn}}(x)+(2q_j)\,\mathrm{coord}_{q_j}$, where $D_j^{\mathrm{HamDyn}}$ is the Frechet data of the HamDyn local cell and $\mathrm{coord}_{q_j}$ is the configuration coordinate functional.
background
The ambient module is the Wave C3 gap5 vacuum-sector kill of unconditioned CanonicalMom rigidity. On the two-site periodic lattice the phase space is pairs $(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. Configuration coordinates appear as continuous linear functionals $\mathrm{coord}_{q_i}$.
HamDyn supplies a local cell density and matching Frechet data $D_j^{\mathrm{HamDyn}}$ (product-rule expansion of kinetic plus gradient terms, scaled by $1/2$). The vacuum-shifted density adds the zero-gradient smear term $q_j^2$ at each site; its Frechet contribution is exactly $2q_j,dq_j$.
This definition packages that sum as a single continuous linear map, parallel to the global vacuum smear derivative $\sum_j N_j\cdot(q_j,\mathrm{coord}{q_j}+q_j,\mathrm{coord}{q_j})$.
proof idea
Pure definitional construction, not a tactic proof. The body is the sum of two continuous linear maps: the upstream HamDyn local-cell Frechet data at site $j$, plus scalar multiplication of the configuration coordinate functional $\mathrm{coord}_{q_j}$ by the real coefficient $2q_j$. No lemmas are applied; the equality to profile partials and the HasFDerivAt certificate are separate downstream lemmas.
why it matters
Supplies the candidate Frechet map used by hasFDerivAt_vacuumShiftLocalCell_raw (proving the vacuum-shifted local profile is differentiable with this derivative) and by vacuumShiftLocalCellD_eq_profilePartials (expanding it into Ha, Hb, Hp coefficient form). Those lemmas underwrite the vacuum-sector kill: the unconditioned CanonicalMom rigidity Prop is false because the ham–ham alternating FE is blind to the vacuum term $a^2$, yet the density is nonconstant on coincident configurations. The repaired terminal is the vacuum-modulo statement; whether structure-nonconstant plus the FE still forces the kinetic/gradient sectors remains open. Binding: D-qg-hkt-rigidity-gauge-scope-20260723.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.