pderivQ_HamDyn
plain-language theorem explainer
The configuration partial of the two-site dynamic Hamiltonian equals the frozen inverse-metric contribution plus the explicit correction N_j q_j (Δq_j)². Residual auditors in the Wave C2 gravity stack cite it when comparing honest Frechet derivatives to frozen HamW partials. The proof evaluates the Frechet derivative of the unfolded Hamiltonian on the q_j basis vector and collapses the two-site sum by indicator arithmetic.
Claim. For any lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, site $j\in\mathbb{Z}/2\mathbb{Z}$, and phase-space point $x=(q,p)$ on two sites, the configuration partial of the dynamic Hamiltonian is $\partial_{q_j}H_{\mathrm{dyn}}(N)(x)=N_{j-1}(1+q_{j-1}^2)(q_j-q_{j-1})-N_j(1+q_j^2)(q_{j+1}-q_j)+N_j q_j(q_{j+1}-q_j)^2$, where $H_{\mathrm{dyn}}(N)(x)=\sum_i(N_i/2)\bigl(p_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr)$.
background
This module closes the first two typed residuals of the Wave C2 Gap5 residual DAG: R0 (decoy) and R1 (honest dynamic structure-function bracket) on a two-site discrete phase space. Coordinates are pairs $(q,p)$ with sites indexed by $\mathbb{Z}/2\mathbb{Z}$.
The dynamic Hamiltonian is the unfolded form used for Frechet calculus: at each site $i$, the density is $(N_i/2)\bigl(p_i^2+(1+q_i^2)(\Delta q_i)^2\bigr)$, where $1+q_i^2$ is the concrete dynamic inverse metric $g(x)$ and $\Delta q_i=q_{i+1}-q_i$. A frozen construction would treat $g$ as an external weight and reuse frozen partials; the honest derivative must also differentiate through $g$.
The configuration partial is the Frechet derivative of the Hamiltonian applied to the basis vector that is $1$ in the $q_j$ slot and zero elsewhere. The doc-comment states the claim as the frozen HamW contribution plus the $\partial g/\partial q$ correction $N_j q_j(\Delta q_j)^2$.
proof idea
Unfold the configuration partial via the Frechet derivative of the dynamic Hamiltonian and expand that derivative as a sum of continuous linear maps (one summand per site). For each site $i$, evaluate the summand on the basis vector $(\mathbf{e}_j,0)$ in phase space.
After simplifying products and splitting on the indicators $i=j$ and $i+1=j$, each summand reduces to three terms: a forward difference contribution, a backward difference contribution, and the quadratic $q_i(\Delta q_i)^2$ correction, each multiplied by the corresponding $0/1$ indicator.
Rewrite the full sum by these simplified summands, distribute over addition and subtraction, then apply the two-site indicator-sum lemmas that collapse $\sum_i f(i)\cdot\mathbf{1}{i=j}$ and $\sum_i f(i)\cdot\mathbf{1}{i+1=j}$. The ring identity $j-1+1=j$ finishes the rewrite to the claimed three-term formula.
why it matters
This is the honest configuration partial required for both R0 and R1 of Wave C2 Gap5. Downstream, the R0 decoy theorem evaluates it at the decoy phase point with the decoy lapse and shows the naive frozen-partial lookalike differs by the uncompensated $\partial g/\partial q$ term. The R1 headline identity for the Hamiltonian-Hamiltonian bracket simp-unfolds this partial (together with the momentum partial) and recovers the exact dynamic structure function for the two-site concrete inverse metric; the extra derivative terms cancel in that bracket.
It also feeds the mixed momentum-Hamiltonian bracket in the HKT point-split target. The module doc is explicit that this work does not flip gap5_constraint_recovery, and continuum and HKT residuals remain open. In the Recognition gravity stack this is discrete structure-function bookkeeping on $n=2$, not a continuum GR claim and not a forcing-chain (T0-T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.