hamDynLocalCellD_eq_profilePartials
plain-language theorem explainer
On the two-site phase space, the Fréchet data of the local Hamiltonian cell equals the linear combination of the three coordinate projections weighted by the profile partials Ha, Hb, Hp. Differentiability proofs for the HamDyn local profile and vacuum-shift variants cite this identity. The argument is extensionality of continuous linear maps followed by simplification and a ring close.
Claim. For each site $j \in \mathbb{Z}/2\mathbb{Z}$ and phase-space point $x=(q,p)$, the continuous linear map giving the local Hamiltonian cell Fréchet data equals $H_a(q_j,q_{j+1},p_j)\,dq_j + H_b(q_j,q_{j+1},p_j)\,dq_{j+1} + H_p(q_j,q_{j+1},p_j)\,dp_j$, where $H_a,H_b,H_p$ are the three partials of the local Hamiltonian profile.
background
The ambient module repairs the CanonicalMom class for Wave C2 gap5 (binding design D-qg-hkt-rigidity-route-20260722). Session B defines the honest HamDyn inhabitant of HKTPointSplitTargetDynCanonicalMom on two sites and separates the balanced quartic falsifier; no ledger flag is flipped.
Phase space is the product of configuration and momentum coordinates indexed by $\mathbb{Z}/2\mathbb{Z}$. The local Hamiltonian cell Fréchet data is the continuous linear map obtained from Mathlib's product-rule expansion of the numerator, scaled by $1/2$. The three scalar coefficients $H_a,H_b,H_p$ are the partial derivatives of that local profile with respect to the two neighboring configuration values and the on-site momentum.
Coordinate projections $dq_j$, $dq_{j+1}$, $dp_j$ are the continuous linear maps extracting those components. The identity rewrites the expanded Fréchet data in the profile-partial basis used by downstream differentiability lemmas.
proof idea
Apply continuous-linear-map extensionality and evaluate both sides on an arbitrary phase-space vector $v$. Unfold the cell Fréchet data and the three profile partials, together with the add/smul/sub rules for continuous linear maps and the coordinate-projection applications. After smul_eq_mul and zero_add, the two sides are identical as polynomials in the coordinates of $x$ and $v$; close by ring.
why it matters
This is the algebraic bridge from the expanded Fréchet definition of the local Hamiltonian cell to the profile-partial form required by Mathlib's HasFDerivAt API. The immediate parent is the lemma establishing Fréchet differentiability of the local Hamiltonian profile at every two-site phase-space point; that lemma quotes the right-hand side of this identity as the candidate derivative.
A second consumer is the vacuum-sector kill path: the vacuum-shift cell Fréchet identity is obtained by starting from this HamDyn equality and adding the vacuum Fréchet term. Together they support the honest CanonicalMom inhabitant that replaces the strong rigidity route killed in Session A, keeping gap5 constraint recovery false while banking the DEFINED-only CanonicalMom rigidity statement for later sessions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.