quarticZeroMomTarget
plain-language theorem explainer
Explicit quartic zero-momentum decoy inhabiting the weak HKT point-split dynamical target on two sites: quartic Hamiltonian density, identically vanishing momentum density, and a decorative nonconstant structure. Gravity auditors of the Wave C2 repair cite it as the formal witness that the weak schema is decoy-inhabitable. Fields are filled by zero advection/brackets; axioms discharge via vanishing-bracket lemmas and a nondegeneracy witness.
Claim. An explicit inhabitant of the weak HKT point-split dynamical target on $N=2$ sites, with Hamiltonian density the quartic density, momentum density identically zero, structure function $1+q_j^2$, vanishing advection and Mom-bracket densities, satisfying differentiability, locality, covariance, the three Poisson identities (Mom-Mom, Mom-Ham split, Ham-Ham), and nondegeneracy.
background
Wave C2 repair (module setting) responds to the adversarial finding that the weak point-split HKT target is decoy-inhabitable. The weak class packages Hamiltonian and momentum densities on phase space for $N=2$ sites (configuration and momentum coordinates indexed by $\mathbb{Z}/2\mathbb{Z}$), a structure function, advection slots, and a Mom-bracket density, plus axioms: differentiability, locality/covariance of ham and structure, three Poisson identities, and nondegeneracy.
The decoy uses the quartic Hamiltonian density (pure-$\pi$ generators), the zero momentum density, and the decorative structure $1+q_j^2$. Upstream, bracket_zeroMom2_any shows any linear combination of zero-momentum density Poisson-commutes with every observable; bracket_quarticHam2_quarticHam2 shows two quartic Hamiltonians Poisson-commute (both sides vanish). Differentiability of the quartic ham and of zero momentum, and nonconstancy of the decorative structure, are already proved in-module.
The strong class later adds load-bearing momentum (nonzero Mom-Mom brackets), advection tied to the Mom-Ham calculus, and kinetic regularity. This definition is the explicit weak inhabitant the critic found.
proof idea
Structure-value definition: set ham density to the quartic density, mom density to zero, structure to the decorative $1+q_j^2$, and all advection and mom-bracket density slots to the zero function.
Differentiability of ham is differentiable_quarticHam2 after unfolding the density wrapper; mom differentiability is differentiable_zeroMom2. Structure nonconstancy is decorativeStructure2_not_constant. Locality of ham and structure are rewrites along equal coordinates; ham covariance is rfl.
Mom-Mom and Mom-Ham split both reduce by bracket_zeroMom2_any (LHS vanishes by zero mom; RHS vanishes by zero mom-bracket density or zero advection). Ham-Ham reduces by bracket_quarticHam2_quarticHam2 (LHS vanishes for pure-$\pi$ generators; RHS has a zero mom-density factor). Nondegeneracy is the packaged witness quarticNondegPhase with the quartic density nondegeneracy lemma.
why it matters
Formal witness that the weak point-split schema is decoy-inhabitable (Codex pass D-qg-hkt-pointsplit-adjudication-20260722). Without this object, the weak class could be mistaken for a load-bearing grind target; with it, rigidity over the weak class is demoted.
Downstream: quarticZeroMomTarget_mom_vanishes records identical vanishing of mom density; quarticZeroMom_fails_mom_load_bearing shows Mom-Mom brackets never fire (the strengthening field that kills the decoy); quarticZeroMomTarget_not_strong proves it does not inhabit the strong class; strong_target_discriminates_decoy is the discrimination receipt (honest strong inhabitant exists; this decoy fails strong). Also referenced from the weak-target module's zero-density nondegeneracy discussion.
In the broader RS gravity stack this is scaffolding hygiene, not a physics law: it forces the binding rigidity statement off the weak class onto CanonicalMom. No ledger flag flips; the eight-tick / $D=3$ forcing chain is untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.