pderivP_HamDyn
plain-language theorem explainer
On the two-site phase space, the momentum partial of the dynamic Hamiltonian HamDyn(N) at site j equals N_j times the momentum coordinate p_j. The configuration-dependent inverse-metric factor never enters this slot. Anyone computing Hamiltonian brackets or HKT kinetic witnesses cites this identity. The proof evaluates the Frechet derivative of HamDyn on the pure-momentum basis vector and collapses the two-site sum by an indicator.
Claim. Let $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ be a lapse assignment, $j\in\mathbb{Z}/2\mathbb{Z}$, and $x=(q,p)$ a point of the two-site phase space. Write $\mathrm{Ham}_{\mathrm{dyn}}(N)$ for the dynamic Hamiltonian $\sum_i (N_i/2)\bigl(p_i^2+(1+q_i^2)(\Delta q_i)^2\bigr)$. Then the partial derivative of $\mathrm{Ham}_{\mathrm{dyn}}(N)$ with respect to the momentum coordinate at site $j$ equals $N_j\,p_j$.
background
Module Wave C2 R0+R1 builds the dynamic structure-function bracket on two lattice sites. The naive decoy that reuses frozen HamW partials fails because the configuration partial picks up an uncompensated $\partial g/\partial q$ term (residual R0). Residual R1 asks for an honest Frechet derivative of the candidate Hamiltonian that includes those metric derivatives, so that the Hamiltonian–Hamiltonian bracket recovers the target dynamic structure function.
HamDyn N is the unfolded two-site Hamiltonian used for Frechet calculus: a sum over $i\in\mathbb{Z}/2\mathbb{Z}$ of $(N_i/2)$ times kinetic $p_i^2$ plus a configuration factor $(1+q_i^2)(\Delta q_i)^2$. Its Frechet derivative is packaged as the continuous linear map HamDynD, and hasFDerivAt_HamDyn certifies that this map is indeed the derivative at every phase-space point.
Momentum partials pderivP extract the directional derivative along the pure-momentum basis vector $(0,e_j)$. Because the inverse-metric factor depends only on configuration, the kinetic slot of the momentum partial is expected to match the frozen case: $\partial_{p_j}\mathrm{Ham}_{\mathrm{dyn}}(N)=N_j p_j$.
proof idea
Unfold pderivP as evaluation of the Frechet derivative on $(0,\mathbf{1}_j)$. Replace that derivative by HamDynD via hasFDerivAt_HamDyn, then distribute over the two-site sum with ContinuousLinearMap.sum_apply.
For each summand $i$, evaluate the scaled linear combination of coordinate maps on $(0,\mathrm{Pi.single},j,1)$. All configuration-coordinate contributions vanish on a pure-momentum direction; only the doubled $p_i,\mathrm{coordP},i$ term survives, and Pi.single_apply plus a case split on $i=j$ yields $(N_i p_i)\cdot\mathbf{1}_{i=j}$. A final ring cleans each branch.
Congruence of the finite sum and the standard identity sum_mul_ite collapse the indicator sum to the single term $N_j p_j$.
why it matters
This is the momentum half of the honest partials needed for residual R1. The headline theorem bracket_HamDyn_HamDyn simp-reduces the dynamic Hamiltonian–Hamiltonian bracket by quoting both pderivQ_HamDyn and pderivP_HamDyn, recovering the exact two-site dynamic structure function for the concrete inverse metric.
Downstream HKT work reuses the same identity: bracket_MomDyn_HamDyn expands the momentum–Hamiltonian bracket; bracket_HamDyn_VacSmear and the vacuum-shift strong target need the kinetic momentum factor; hamDyn_kinetic_regular_witness checks nondegeneracy of the kinetic partial at a concrete phase point.
Within the Seven Gaps gravity stack this closes the Frechet bookkeeping for the dynamic structure function on $n=2$. It does not flip gap5_constraint_recovery; continuum and remaining HKT residuals stay open. The result is local discrete calculus, not a continuum GR identity, but it is the algebraic engine that lets the dynamic bracket match the target structure function once configuration partials are handled honestly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.