quarticBalancedWeakTarget
plain-language theorem explainer
The balanced quartic Hamiltonian–momentum pair on two labels is packaged as an inhabitant of the weak point-split dynamical target class at N=2. Gravity and HKT-rigidity workers cite it as the base witness before strengthening advection and load-bearing slots. The body is a structure instance: densities and structure function are plugged in, then locality, covariance, Poisson identities, and nondegeneracy are discharged by sibling lemmas and a Z/2 balance identity.
Claim. There is an inhabitant of the weak point-split dynamical target schema at two labels whose Hamiltonian density, momentum density, and structure function are the balanced quartic data. The instance supplies differentiability of the summed Hamiltonian and momentum, locality and covariance of the Hamiltonian density, locality of the structure function, vanishing of the momentum–momentum and Hamiltonian–Hamiltonian brackets (the latter via balance), the split momentum–Hamiltonian bracket identity, and a nondegeneracy 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 strong point-split target at N=2 by a balanced quartic falsifier and proves that strong-class rigidity fails. Session B separates CanonicalMom; the ledger flag gap5_constraint_recovery stays false.
A ledger state is balanced when debit equals credit (double-entry prior to any cost functional). That constraint is used so momentum-coordinate selection does not depend on where a cost vanishes. The weak target class asks for Hamiltonian and momentum densities, a structure function, advection maps, a momentum-bracket density, plus analytic and algebraic axioms: differentiability, locality, covariance, Poisson bracket relations, and nondegeneracy.
Sibling data supply the balanced quartic densities and structure on Z/2 labels, the balanced momentum functional, and the balance identity that equates the two label-wise structure–momentum products. Upstream Z/2 arithmetic (zero-plus-one, one-plus-one) collapses two-term sums in the Hamiltonian–Hamiltonian bracket check.
proof idea
Structure instance for the weak target at N=2. Fields are filled by the balanced quartic Hamiltonian density, momentum density, structure function, advection maps, and momentum-bracket density.
Differentiability of the summed Hamiltonian reduces by funext and simp to the known differentiable quartic Hamiltonian; momentum differentiability is the balanced-momentum lemma. Structure nonconstancy is a named sibling. Locality and covariance of the Hamiltonian density, and locality of the structure function, are direct rewrites.
Momentum–momentum bracket is the balanced-momentum Poisson identity. Momentum–Hamiltonian split rewrites the summed density to the balanced quartic Hamiltonian and applies the corresponding bracket lemma. Hamiltonian–Hamiltonian is the delicate step: the left bracket vanishes by the balanced-quartic self-bracket; the right-hand structure–momentum sum is rewritten via sum over Z/2 and the two successor identities, then balance forces the two structure–momentum products equal, so the antisymmetric coefficient times their difference is zero. Nondegeneracy is a phase witness paired with a density nondegeneracy fact at label 0.
why it matters
This is the weak base of the balanced-quartic falsifier in gap5 Session A. Downstream, the strengthened inhabitant is built by extending this instance with load-bearing momentum and honest advection ties; the strong-class rigidity negation then feeds the strong target into the rigidity statement and obtains a contradiction by forcing p^4 = c_Kin p^2 + c_Vac at three momenta.
In the Recognition gravity ledger, the point-split dynamical schema is the local functional-equation interface against which HKT-style rigidity claims are tested. Packaging the balanced quartic at the weak level separates pure Poisson and locality content from the stronger load-bearing and advection axioms, so the later CanonicalMom repair can keep the honest HamDyn inhabitant while excluding this quartic from the repaired class. No continuum magic-4 multiplier or ledger recovery flag is claimed here; the declaration only banks the weak inhabitant used to kill strong rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.