hasFDerivAt_hamDynLocalCell
plain-language theorem explainer
Fréchet differentiability of the local honest-HamDyn density cell on two-site phase space, with derivative written as the Ha/Hb/Hp-weighted sum of coordinate projections. Gravity workers cite it when packaging LocalHamSmooth for the CanonicalMom HamDyn inhabitant. Proof is a one-line rewrite identifying that linear map with the raw cell derivative, then applying the raw HasFDerivAt lemma.
Claim. For each site $j\in\mathbb{Z}/2\mathbb{Z}$ and each $x$ in two-site phase space, the map $y\mapsto \tfrac12\bigl(p_j(y)^2+(1+q_j(y)^2)(q_{j+1}(y)-q_j(y))^2\bigr)$ is Fréchet differentiable at $x$, and its derivative is $H_a\,dq_j+H_b\,dq_{j+1}+H_p\,dp_j$, where $H_a,H_b,H_p$ are the local partial profiles of that density evaluated at $(q_j(x),q_{j+1}(x),p_j(x))$.
background
Module setting is Wave C2 gap5: inhabit the CanonicalMom HamDyn target on $N=2$ and bank the DEFINED-only rigidity statement, without flipping the ledger flag. The local density profile is $$H(a,b,p)=\tfrac12\bigl(p^2+(1+a^2)(b-a)^2\bigr),$$ written with the constant $\tfrac12$ so Mathlib's product rule matches the recorded Frechet data.
The three partial profiles $H_a$, $H_b$, $H_p$ are the explicit algebraic factors that appear in the product-rule expansion (scaled by $\tfrac12$). Coordinate maps $q_j$ and $p_j$ extract the configuration and momentum components at site $j$ on PhaseSpace 2. Upstream, hasFDerivAt_hamDynLocalCell_raw already proves differentiability with derivative equal to the bundled cell map hamDynLocalCellD; the companion identity hamDynLocalCellD_eq_profilePartials expands that cell map into the Ha/Hb/Hp linear combination of coordinate functionals.
proof idea
One-line term proof. Rewrite the claimed derivative expression via hamDynLocalCellD_eq_profilePartials (which equates the bundled cell derivative to the Ha/Hb/Hp-weighted sum of coordQ j, coordQ (j+1), and coordP j). The goal becomes exactly the statement of hasFDerivAt_hamDynLocalCell_raw, which is applied directly. No new calculus is done here; the raw lemma already chains Frechet rules on the coordinate projections and the polynomial profile.
why it matters
This lemma is the sole hasFDerivCell field of hamDynLocalSmooth, the LocalHamSmooth instance for the honest HamDyn density. That instance is the smoothness witness required by the CanonicalMom HamDyn inhabitant of HKTPointSplitTargetDynCanonicalMom (Session B of the gap5 binding design). Without an explicit Frechet derivative matching the recorded partials, the CanonicalMom class cannot be inhabited honestly, and the DEFINED-only rigidity statement for $N=2$ cannot be banked. Downstream sessions C are expected to prove that rigidity statement; this cell derivative is infrastructure, not the rigidity claim itself. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is touched directly; the work sits in the gravity SevenGaps layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.