LocalHamSmooth_hb_unique
plain-language theorem explainer
Any two smooth witnesses for the same local Hamiltonian density agree on the configuration-slot partial with respect to the second lattice site. Gravity and continuum-limit workers cite this when the kinetic-normalized rigidity chain needs a canonical hb coefficient. The proof is Fréchet uniqueness of the cell derivative, evaluated on the unit bump in the second configuration coordinate.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian density profile. If $S_1$ and $S_2$ are two $C^1$ witnesses for $h$ (each supplying continuous partials $h_a,h_b,h_p$ together with a Fréchet derivative identity on every two-site cell), then for all $a,b,p\in\mathbb{R}$ one has $S_1.h_b(a,b,p)=S_2.h_b(a,b,p)$.
background
The ambient setting is the two-site periodic lattice phase space: pairs $(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. A local Hamiltonian profile is simply a map $h(a,b,p)$ of neighboring configurations and one conjugate momentum. A smooth witness packages three coefficient profiles (partials in $a$, $b$, and $p$) plus a cellwise Fréchet derivative identity that recovers those coefficients.
The module closes gap 5 of the HKT gravity ledger: after the mod-vacuum kill, kinetic-normalized canonical momentum rigidity must pin the local density uniquely. The configuration cell map fePhase embeds scalars $(a,b,p,r)$ into phase space; the private evaluation lemma localCellD_eval_b0 shows that the Fréchet derivative of the cell, applied to the unit bump in the second configuration slot, returns exactly the $h_b$ coefficient of the witness.
Upstream, hasFDerivAt_localCell states that every smooth witness really does supply a Fréchet derivative for the cell functional $y\mapsto h(y_1(j),y_1(j+1),y_2(j))$.
proof idea
Build the phase-space point $x=$ fePhase $a,b,p,0$. Both witnesses give a Fréchet derivative of the same cell map at $x$ (via hasFDerivAt_localCell at slot $j=0$). Mathlib's HasFDerivAt.unique therefore equates the two continuous linear maps. Congruence under evaluation on the tangent vector $(\mathbf{e}_1,0)$ (unit bump in the second configuration coordinate) yields equality of the two scalar values. The private evaluation lemma rewrites each side as the corresponding $h_b(a,b,p)$, finishing the proof.
why it matters
Kinetic-normalized rigidity needs a single, witness-independent $h_b$ before the FTC recovery and intensivity field can be stated as theorems rather than class assumptions. This uniqueness lemma discharges that bookkeeping for the second configuration slot, matching the Fréchet-uniqueness pattern already used for the other coefficient slots in the same module.
It sits inside Wave C4/C5 gap 5 (binding D-qg-hkt-modvacuum-verdict / D-gap5-acceptance-adjudication): after the mod-vacuum kill rules out non-normalized kinetic sectors, the remaining freedom in smooth local densities must collapse. No downstream consumers are wired yet in the graph; the lemma is terminal scaffolding for the coefficient-extraction layer that feeds Gap5ConstraintCloseStatus.
Framework-wise this is continuum bookkeeping on the lattice Hamiltonian, not a T0–T8 forcing step, but it is required before any claim that the Recognition-side gravity density is uniquely determined by its profile.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.