localCellD_eval_b0
plain-language theorem explainer
Evaluates the local cell differential of a smooth local Hamiltonian profile at the free-energy phase point with cell tag 0, on the unit configuration direction in the complementary Z/2 slot. The value is exactly the hb coefficient of the smoothness witness. Used when matching Frechet derivatives of the profile map to hb. Proof is two simp rounds unfolding localCellD, fePhase, and Pi.single.
Claim. Let $h$ be a local Hamiltonian profile with smoothness witness $S$, and let $a,b,p\in\mathbb{R}$. The local cell differential of $h$ at cell $0\in\mathbb{Z}/2\mathbb{Z}$, evaluated at the free-energy phase point built from $(a,b,p)$ with tag $0$, on the tangent vector that is the unit basis vector in the complementary configuration slot and zero in momenta, equals the coefficient $S.h_b(a,b,p)$.
background
Module setting is Wave C4/C5 gap5: after the mod-vacuum kill, the remaining work is kinetic-normalized rigidity for the HKT (Hamilton–Killing-type) local functional equation. Profiles live on a two-cell phase space indexed by $\mathbb{Z}/2\mathbb{Z}$; a free-energy phase constructor packages real coordinates $(a,b,p)$ with a cell tag into a full phase-space point.
A local Hamiltonian profile carries a density; a smoothness witness supplies continuous linear data for its first derivatives, including an $h_b$ slot for the $b$-direction. The local cell differential is the cell-wise first variation of that density: it pairs configuration and momentum coordinate maps against the witness coefficients.
The present evaluation is the $b$-slot companion of the $a$- and $p$-slot evaluations. Downstream Frechet uniqueness and derivative identification both reduce to reading one such pairing at a canonical phase point.
proof idea
Pure definitional evaluation, no analysis. First simp only unfolds the local cell differential into continuous-linear-map addition and scalar multiplication, applies the configuration and momentum coordinate maps, multiplies scalars, expands the free-energy phase constructor, and rewrites the cell index via the $\mathbb{Z}/2$ identity $0+1=1$. Second simp resolves Pi.single on the complementary slot: same-index gives $1$, off-index (proved by decide) gives $0$. The surviving term is exactly $S.h_b(a,b,p)$.
why it matters
Gap5 terminal work needs the $h_b$ coefficient of any smoothness witness to be intrinsic: independent of the witness and equal to the Frechet derivative of the profile map in the $b$-direction. This lemma is the evaluation step both parents call.
LocalHamSmooth_hb_unique builds the free-energy phase point, invokes uniqueness of Frechet derivatives of the local cell map, and needs this identity to read the $h_b$ slot off either witness. LocalHamSmooth_hb_eq_fderiv likewise reduces the Frechet derivative of profileMap along $(0,1,0)$ to the same pairing.
In the Recognition gravity stack this closes the $b$-channel of kinetic-normalized CanonicalMom rigidity after the vacuum-sector kill, so the constraint-recovery flip for gap5 can bind on the kinetic-normalized half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.