hamAdvTo_eq_computed
plain-language theorem explainer
At two sites, the momentum–Hamiltonian point-split axiom forces each target's forward advection slot to equal the Mom–Ham Poisson-bracket extraction. Builders of strong HKT point-split inhabitants cite this to discharge the advection-tied field. The proof collapses a two-term site-projector sum to the single nonzero slot and matches it to the bracket via the split axiom.
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 target's forward advection coefficient at $(x,j)$ equals the Mom–Ham bracket-calculus extraction of that coefficient (the value obtained by smearing momentum at site $j$ against Hamiltonian density at site $j+1$).
background
This module repairs the weak point-split HKT schema after an adversarial pass showed it is decoy-inhabitable by quartic zero-momentum models. The weak class keeps free advection slots; the strengthened class ties those slots to Mom–Ham bracket calculus, demands load-bearing momentum, and requires kinetic regularity.
The two-site index set is $\mathbb{Z}/2\mathbb{Z}$. Site projectors siteDelta j are the standard Kronecker indicators on that set (value $1$ on the matching site, $0$ elsewhere). The target axiom mom_ham_split equates a Poisson bracket of smeared momentum and Hamiltonian densities to a linear combination of the advection slots hamAdvFrom and hamAdvTo. The sibling definition computedHamAdvTo is exactly that bracket extraction for the forward slot.
The local claim is the $n=2$ specialization: under the split axiom, the free forward slot is forced equal to the computed bracket value. The companion lemma does the same for the backward slot.
proof idea
Apply the target's mom_ham_split at the smeared pair (siteDelta j, siteDelta (j+1)). Unfold the definition of the computed forward advection. The resulting two-site sum collapses by Finset.sum_eq_single j: the diagonal term uses siteDelta_self (value $1$) and zmod2_succ_ne (so the cross projector is $0$), while off-diagonal summands vanish by the projector definition. Transitivity identifies the Poisson bracket with T.hamAdvTo x j. A final linarith closes the equality with the unfolded computed value.
why it matters
This lemma is the discharge step for the strengthened advection-tied obligation: strong inhabitants must set forward advection equal to the bracket extraction, not a decorative free field. Downstream, hamDynPointSplitTargetStrong, quarticBalancedStrongTarget, vacuumKineticStrongTarget, and vacuumShiftStrongTarget all invoke it (or its sibling) when filling advTo_tied / advFrom_tied.
It sits inside Wave C2 of the SevenGaps gravity program: exclude decoys from the point-split HKT class so that rigidity claims are load-bearing. The strong-class rigidity statement itself is already proven false by the balanced-quartic inhabitant; binding rigidity moves to the CanonicalMom class. This equality remains necessary infrastructure for every honest strong inhabitant and for the discrimination gate (honest HamDyn passes; quartic zero-momentum fails mom_load_bearing).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.