hktPointSplitTargetDynStrong_two_nonvacuous
plain-language theorem explainer
The strengthened point-split HKT target at two sites is inhabited: there exists at least one honest dynamical package meeting load-bearing momentum, bracket-tied advection, and kinetic regularity. Gravity and HKT-rigidity workers cite it as the non-vacuity half of the discrimination gate against quartic zero-momentum decoys. The proof is a one-line term witness via the honest HamDyn inhabitant.
Claim. The type of strengthened point-split HKT dynamical targets on $n=2$ sites is nonempty: there exists a structure extending the weak point-split schema that also satisfies (i) nontrivial $\{\mathrm{Mom},\mathrm{Mom}\}$ bracket for the momentum density, (ii) advection slots equal to the Mom–Ham bracket-calculus extractions, and (iii) kinetic regularity (some smeared-Ham momentum partial nonzero).
background
Wave C2 repair after an adversarial pass showed the weak point-split HKT target is decoy-inhabitable by a quartic zero-momentum package, so rigidity over that weak class is not load-bearing. The strong target extends the weak schema with three critic strengthenings: load-bearing momentum (nontrivial ${\mathrm{Mom},\mathrm{Mom}}$ bracket), advection slots forced equal to the Mom–Ham bracket-calculus values rather than free decorative choices, and kinetic regularity excluding purely potential densities.
The honest HamDyn package is the concrete inhabitant of the strong class at $n=2$. It reuses the weak HamDyn point-split target and discharges the three extra fields (momentum load-bearing via an explicit phase-space witness, advection tied to the computed bracket extractions, and kinetic regularity). The weak schema is retained only as documentation of the critic finding; discrimination requires an honest pass and a decoy fail on the strong class.
proof idea
One-line term proof. Nonemptiness of the strong target at $n=2$ is witnessed by packaging the honest HamDyn inhabitant as an explicit term of that structure type. No further tactic work: the def already fills the extended fields (load-bearing momentum, tied advection, kinetic regularity) on top of the weak HamDyn base.
why it matters
Closes the non-vacuity half of the discrimination receipt: honest packages inhabit the strong class while the quartic zero-momentum decoy is excluded. Downstream, strong_target_discriminates_decoy conjoins this nonemptiness with the decoy-exclusion lemma. The same nonemptiness feeds the (now dead) strong-class rigidity statement at $n=2$, which is proven false by a balanced-quartic inhabitant elsewhere; binding rigidity moves to the CanonicalMom class. In the SevenGaps gravity stack this is bookkeeping after the critic pass, not a new physical law: it certifies that the strengthened grind target is still live for honest dynamics while blocking the decoy route that voided weak-class rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.