localCellD_eval_p0
plain-language theorem explainer
Evaluating the local cell differential of a smooth Hamiltonian profile at cell 0, on the phase point (a,b,p,0), against the pure π₀ unit direction recovers the profile's momentum slot hp(a,b,p). Gravity/HKT rigidity arguments cite this when identifying hp with a Fréchet derivative or proving hp is witness-independent. The proof is a short simp expansion of localCellD, coordinate maps, and ZMod-2 arithmetic.
Claim. Let $h:\mathbb{R}^3\to\mathbb{R}$ be a local Hamiltonian profile and $S$ a smooth witness supplying partials $h_a,h_b,h_p$. Write $x=(q_0,q_1,\pi_0,\pi_1)=(a,b,p,0)$ and let $v$ be the phase-space vector with only $\pi_0$-component equal to $1$. Then the continuous linear map $\mathrm{localCellD}(h,S)$ at cell $j=0$ and basepoint $x$, applied to $v$, equals $h_p(a,b,p)$.
background
This module closes Wave C4/C5 gap5 for HKT gravity: after killing the mod-vacuum rigidity statement, one upgrades to kinetic-normalized CanonicalMom rigidity, with FTC recovery theorem-derived rather than assumed.
A LocalHamProfile is a map $h:\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ (two neighboring configuration slots and one momentum). LocalHamSmooth h packages candidate partials ha, hb, hp together with a cellwise Fréchet hypothesis tying them to $h$. The differential localCellD at cell $j$ is the continuous linear form
$(S.ha),\mathrm{coord}Q_j+(S.hb),\mathrm{coord}Q_{j+1}+(S.hp),\mathrm{coord}P_j$
evaluated on the neighboring pair $(q_j,q_{j+1},\pi_j)$.
fePhase a b p r packs the four-tuple $(a,b,p,r)$ into 2-cell phase space. Coordinate projections coordQ/coordP extract configuration and momentum components; on $\mathbb{Z}/2\mathbb{Z}$, $0+1=1$.
proof idea
Term-mode proof by two simp passes. Unfold localCellD into the three scaled coordinate maps, then apply continuous-linear-map add/smul rules, coordQ_apply, coordP_apply, and smul_eq_mul. Substitute fePhase a b p 0 so the basepoint has $q_0=a$, $q_1=b$, $\pi_0=p$, $\pi_1=0$, and use zmod2_zero_add_one for the neighbor index. The test vector is $(0,\mathrm{Pi.single},0,1)$: configuration components vanish and only the $\pi_0$ slot is 1, so Pi.single_eq_same kills the ha/hb terms and leaves exactly S.hp a b p.
why it matters
Identifies the abstract momentum slot hp with a concrete directional evaluation of the cell differential. Downstream, LocalHamSmooth_hp_unique uses this (via uniqueness of Fréchet derivatives of localCell) to prove hp is independent of the smooth witness. LocalHamSmooth_hp_eq_fderiv further equates S.hp a b p to the Fréchet derivative of the profile map in the pure-$p$ direction.
That uniqueness/identification is part of the kinetic-normalized rigidity terminal for gap5: once momentum partials are canonically fixed, the intensivity field and FTC recovery (ftc_recovery_of_normalized) can close without an assumed class field. In the broader SevenGaps gravity program this is bookkeeping for the HKT local functional equation, not a T0–T8 forcing step, but it is required infrastructure for the gap5 acceptance adjudication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.