bracket_HamDyn_HamDyn

Wave C2 of the SevenGaps gravity residual DAG targets the dynamic structure-function bracket on a two-site lattice. The module closes residuals R0 and R1 from the QG Wave C2 draft: R0 shows that naively plugging a configuration-dependent inverse metric into the frozen Hamiltonian slot fails, because the configuration partial picks up an uncompensated $\partial g/\partial q$ term. R1 asserts that the same candidate, once its Fréchet derivative is computed honestly, still yields the target dynamic structure function in the Hamiltonian–Hamiltonian bracket.

The dynamic Hamiltonian HamDyn N is the unfolded two-site form $\sum_i (N_i/2)\bigl(p_i^2+(1+q_i^2)(\Delta q_i)^2\bigr)$, with $\Delta q_i=q_{i+1}-q_i$. The concrete dynamic inverse metric is the local factor $1+q_j^2$. The Poisson bracket is the standard phase-space sum of $\partial_q H,\partial_p K-\partial_p H,\partial_q K$ terms. The honest $q$-partials of HamDyn include the metric-derivative contributions that defeated the decoy; those extras must cancel when both arguments are dynamic Hamiltonians.

This sits inside the discrete Dirac-algebra program for Recognition gravity: the structure function is the lattice avatar of continuum $(NM'-MN')\cdot G\cdot D$ with $G=1+q^2$. Continuum and HKT residuals remain open; this identity does not flip full constraint recovery.

Tactic proof. First simp only unfolds the Poisson bracket and the honest partials pderivQ_HamDyn, pderivP_HamDyn, together with the concrete inverse metric, producing an explicit two-site sum of products of $N$- and $M$-weighted terms.

A named intermediate equality step1 rewrites that sum, sitewise, into $\sum_j(N_{j-1}M_j-M_{j-1}N_j),(1+q_{j-1}^2),p_j(q_j-q_{j-1})$. Each site identity is pure polynomial cancellation (ring under Finset.sum_congr).

After rewriting by step1, sum_reindex 1 shifts the summation index by $+1$ on $\mathbb{Z}/2\mathbb{Z}$. The reindex goal reduces by the ring identity $j+1-1=j$ and a final ring, landing on the target form with factors $(N_j M_{j+1}-M_j N_{j+1}),g_j,p_{j+1}(q_{j+1}-q_j)$.

This is the R1 headline identity of Wave C2: it is the ham_ham field of concreteDynamicHamiltonianConstruction, the inhabitant of PhaseSpaceDependentHamiltonianConstruction for the concrete dynamic inverse metric at $n=2$. That construction immediately yields phaseSpaceDependentDiracPremise_two_site (DAG R2 folded into R1 for two sites).

Downstream, bracket_HamDyn_shape in DiracAlgebraContinuum is a one-line alias, and the continuum Dirac density $(NM'-MN')\cdot G\cdot D$ is the continuum shape sampled from this RHS. The $N$-site module recovers the two-site case via bracket_HamDynN_recovers_bracket_HamDyn and states the analogous identity for HamDynN. HKT residual targets (hamDynPointSplitTarget, vacuumShiftWeakTarget) consume the same bracket shape.

In the Recognition gravity stack this is the discrete structure-function step that lets phase-space-dependent metrics enter the Dirac algebra without spoiling the Hamiltonian–Hamiltonian bracket. It does not close gap5 constraint recovery; continuum and HKT residuals stay open per the module doc.