hamDynPointSplitTargetStrong
plain-language theorem explainer
An explicit Hamiltonian-dynamics model on two lattice sites that meets the strengthened point-split HKT target: nontrivial momentum brackets, advection fixed by the Mom–Ham calculus, and nonzero kinetic response. Gravity and continuum-limit workers cite it as the honest positive witness after the quartic zero-momentum decoy was excluded. The construction packages four short witnesses (load-bearing bracket, two advection equalities, kinetic partial) onto the existing weak HamDyn target.
Claim. There is an explicit two-site Hamiltonian density (the standard HamDyn model) that inhabits the strengthened point-split target: its momentum density yields a nontrivial Poisson bracket $\{M_v,M_w\}\neq 0$ at some phase-space point; its source and target advection slots equal the bracket-calculus extractions from the Mom–Ham split; and some momentum partial of the smeared Hamiltonian is nonzero.
background
Wave C2 of the SevenGaps gravity stack repairs the point-split Hamilton–Kirchhoff–Toda (HKT) target after an adversarial pass showed the weak schema is decoy-inhabitable by a quartic zero-momentum density. The weak class only asks for a Mom–Ham split of the Hamiltonian density into momentum and potential pieces with free advection slots. That is too loose: a pure potential with vanishing momentum still type-checks.
The strengthened structure adds three critic fields. Load-bearing momentum demands smeared momentum functionals whose mutual bracket is nonzero somewhere. Advection tying forces the source and target advection slots to equal the explicit bracket-calculus values computedHamAdvFrom / computedHamAdvTo rather than decorative free data. Kinetic regularity asks that some momentum partial of the smeared Hamiltonian be nonzero, ruling out purely potential densities.
Upstream, under the Mom–Ham split at $n=2$, the lemmas hamAdvFrom_eq_computed and hamAdvTo_eq_computed already identify the free advection slots of any weak target with those bracket extractions. Separate witnesses compute a concrete nonzero ${M_{\delta_0},M_{\delta_1}}$ for HamDyn and a nonzero kinetic partial at a nondegenerate phase point.
proof idea
One-line structure inhabitant: the underlying weak target is the existing HamDyn point-split model. Load-bearing momentum is discharged by packaging the site deltas $\delta_0,\delta_1$ with a fixed witness phase and the pre-proved nonzero bracket hamDyn_mom_load_bearing_witness. Source and target advection tying each reduce, for every phase point and site, to a simpa application of hamAdvFrom_eq_computed / hamAdvTo_eq_computed on the weak HamDyn target. Kinetic regularity is the triple of a nondegenerate phase, site $0$, and the pre-proved nonzero partial hamDyn_kinetic_regular_witness.
why it matters
This is the discrimination-gate positive witness for the strong class: the honest HamDyn model passes, while the quartic zero-momentum decoy is killed by load-bearing momentum. Downstream, hktPointSplitTargetDynStrong_two_nonvacuous is the one-line Nonempty certificate built from this inhabitant. The CanonicalMom repair then extends it further: hamDynPointSplitTargetCanonicalMom sets this strong inhabitant as its base and adds local Hamiltonian and structure profiles.
Module-level consequence: strong-class rigidity is already dead (the balanced-quartic falsifier lives in the CanonicalMom module), so binding rigidity work moves off the plain strong target onto the CanonicalMom class. No ledger flag flips here; the declaration only certifies that the strengthened schema is inhabited by real continuum-motivated dynamics rather than a critic decoy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.