hamAdvFrom_eq_computed
plain-language theorem explainer
At two sites, any dynamical point-split HKT target whose Mom–Ham split holds has source advection slots equal to the Poisson-bracket calculus values. Builders of strong-class inhabitants cite this when discharging the advection-tied field. The proof collapses a two-site sum via the site indicator and finishes by linear arithmetic.
Claim. Let $T$ be a dynamical point-split HKT target at $n=2$, let $x$ be a point of the two-site phase space, and let $j\in\mathbb{Z}/2\mathbb{Z}$. Then the source Hamiltonian advection slot of $T$ at $(x,j)$ equals the value computed from the momentum–Hamiltonian bracket calculus at that slot.
background
This module repairs the Wave C2 point-split HKT target after an adversarial pass showed the weak schema is decoy-inhabitable by quartic zero-momentum models. The strong class adds load-bearing momentum, kinetic regularity, and the requirement that advection slots match the Mom–Ham bracket calculus.
The two-site lattice is indexed by $\mathbb{Z}/2\mathbb{Z}$. The site indicator siteDelta j is the Kronecker delta on that lattice (value $1$ at $j$, $0$ elsewhere). The field mom_ham_split asserts that the Poisson bracket of a momentum density against a Hamiltonian density, tested against a pair of site weights, equals a discrete divergence built from the advection slots hamAdvFrom and hamAdvTo.
The sibling computedHamAdvFrom is the explicit right-hand side obtained by reading those slots off the bracket calculus. The theorem says the target's stored source slots agree with that computation whenever the split axiom holds at $n=2$.
proof idea
Instantiate mom_ham_split on the pair of identical test weights (siteDelta j, siteDelta j) at the given phase point. Unfold the computed source-slot definition. The resulting two-site sum is reduced by Finset.sum_eq_single j: off-diagonal terms vanish because siteDelta j i = 0 for $i\neq j$; the diagonal term uses siteDelta j j = 1 and siteDelta j (j+1) = 0 (the latter from zmod2_succ_ne), leaving exactly $-T.\mathrm{hamAdvFrom},x,j$. Transitivity identifies the bracket with that value; linarith rearranges to the claimed equality.
why it matters
Strong-class inhabitants discharge advFrom_tied by quoting this identity (and its hamAdvTo twin). Downstream users include the honest HamDyn inhabitant hamDynPointSplitTargetStrong, the balanced-quartic strong target in HKTCanonicalMomTarget, the vacuum-kinetic and vacuum-shift strong targets, and the (now false) strong rigidity statement HKTRigidityStatementPointSplitDynN2Strong.
In the SevenGaps gravity program this is bookkeeping, not a new physical law: it makes the advection-tied clause of the strong schema an equality with the bracket calculus rather than a free field. The module doc records that strong-class rigidity is dead (killed by the balanced quartic); binding rigidity moves to the CanonicalMom class. No ledger flag flips here; the discrimination gate is only that honest inhabitants pass and the quartic zero-momentum decoy fails mom_load_bearing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.