quarticBalancedStrongTarget
plain-language theorem explainer
The balanced quartic dynamics package is exhibited as a full inhabitant of the strengthened HKT point-split target class at N=2: honest advection slots, load-bearing momentum, and kinetic regularity. Gravity auditors cite it as the concrete counterexample that kills strong-class rigidity. The construction lifts the weak target and discharges the three strong-class fields by existing witnesses and computed-advection equalities.
Claim. The balanced quartic Hamiltonian–momentum package on two sites is an element of the strengthened HKT point-split dynamical target class at $N=2$: its advection slots equal the computed Hamiltonian advection, its momentum density is load-bearing at a nontrivial phase configuration, and its kinetic sector admits a regular nondegenerate phase witness.
background
Module setting is Wave C2 gap5: kill strong rigidity and repair the CanonicalMom class (binding design D-qg-hkt-rigidity-route-20260722). Session A inhabits the strengthened point-split target at $N=2$ by a balanced-quartic falsifier, then proves strong-class rigidity false. No ledger flag is flipped.
The weak target already packages the balanced quartic Hamiltonian and momentum densities. The strengthened class adds three obligations: momentum must be load-bearing (nontrivial phase dependence), advection-from and advection-to slots must match the computed Hamiltonian advection, and the kinetic sector must be regular (nondegenerate phase witness). Sibling structure MomBalanced and the kinetic-regularity witness supply the concrete data.
Upstream phase infrastructure (eight-tick phases $k\pi/4$, continuum plane-wave phases) is only ambient notation here; the local work is discrete $N=2$ point-split dynamics on $\mathbb{Z}/2$.
proof idea
Structure-instance construction, not a deep proof. The weak-target field is set to the existing balanced-quartic weak package. Load-bearing momentum is a refine of a triple (two deltas, a load phase, and the mom-load-bearing witness), rewritten under MomBalanced. Advection-from and advection-to are one-line simpa applications of the computed-advection equalities for the weak target. Kinetic regularity is the triple of a nondegenerate phase, the zero class in $\mathbb{Z}/2$, and the kinetic-regularity witness.
why it matters
This is the Session A falsifier that makes strong-class rigidity fail. Downstream, not_HKTRigidityStatementPointSplitDynN2Strong feeds the package into the strong rigidity statement and obtains $p^4 = c_{\mathrm{Kin}} p^2 + c_{\mathrm{Vac}}$ at three momenta, a contradiction. Separately, canonicalMom_excludes_balanced_quartic shows the same package does not inhabit the repaired CanonicalMom class, so the decoy is filtered out once the class is tightened. The discrimination receipt strong_target_discriminates_decoy uses the nonempty strong class (witnessed here) against a zero-momentum decoy that fails strong. Framework role: closes the strong-rigidity kill on the HKT point-split route without claiming the CanonicalMom rigidity theorem (Sessions C).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.