unitStructure_recovers_original_ham_ham_RHS
plain-language theorem explainer
The unit-structure Hamiltonian–Hamiltonian right-hand side, which inserts an explicit factor of 1 in front of the momentum density, equals the classical nearest-neighbor advection sum without that factor. Anyone comparing frozen unit structure against the original HKT ham–ham bracket form would cite this identity. The proof unfolds the definition, congruences the finite sum termwise, and finishes by ring.
Claim. For any lattice size $n$, any momentum-density map $\rho$ from phase space to site values, any two real fields $N,M$ on the cyclic lattice $\mathbb{Z}/n\mathbb{Z}$, and any phase-space point $x$, the unit-structure ham–ham RHS equals $\sum_{j}(N_j M_{j+1}-M_j N_{j+1})\,\rho(x)_j$.
background
This module is Wave C2 R5/R6 groundwork for a widened Hojman–Kuchař–Teitelboim (HKT) target that carries an explicit structure-function slot rather than folding structure into momentum density. The classical unsplit advection form is kept as a falsification-adjacent record; the original frozen rigidity statement is already known false at $n=1$.
Phase space is the product of configuration and conjugate momentum on the periodic lattice of $n$ sites. The unit-structure RHS is the sum $\sum_j(N_j M_{j+1}-M_j N_{j+1})\cdot(1\cdot\rho(x)_j)$, i.e. the classical ham–ham advection kernel with an explicit multiplicative unit in place of a nontrivial structure function.
Sibling definitions introduce the dynamic HKT target and the rigidity statement as defined Props, neither proved nor assumed here.
proof idea
One short algebraic identity. Unfold the definition of the unit-structure RHS, which differs from the target sum only by the factor $(1:\mathbb{R})$ in each summand. Apply Finset.sum_congr with reflexive index equality, then ring on each summand to cancel $1\cdot\rho(x)_j$ down to $\rho(x)_j$.
why it matters
Places a clean bridge between the frozen unit-structure placeholder and the classical unsplit ham–ham advection form used in the HKT literature. Downstream the module defines the dynamic rigidity statement and status flags; this identity lets later arguments rewrite unit structure back to the original RHS without bookkeeping noise.
It does not close HKT rigidity. The module doc records that the original rigidity statement fails at one site, that unsplit mom_ham is uninhabitable for smooth nearest-neighbor profiles against the frozen quadratic Hamiltonian at $n=2$, and that the load-bearing class is the strong point-split target. This lemma is bookkeeping groundwork inside that widened target, not a forcing-chain step (T0–T8) or a constants claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.