quarticBalancedHamDensity2_nondeg
plain-language theorem explainer
At the design witness with vanishing configuration and unit momentum on the first site of a two-site register, the balanced quartic Hamiltonian density is nonzero. Authors of the HKT point-split / CanonicalMom repair cite this as the nondegeneracy check that the model is not the zero functional. The proof is a two-step unfold plus numeric normalization of 1^4.
Claim. Let the two-site phase-space point have vanishing configuration coordinates and momentum $\pi=(1,0)$ on $\mathbb{Z}/2\mathbb{Z}$. Then the quartic kinetic density $\pi_j^4$ evaluated at site $j=0$ satisfies $\pi_0^4 \neq 0$.
background
Module context is Wave C2 gap5: kill strong rigidity and repair the CanonicalMom class for the HKT point-split target (binding design D-qg-hkt-rigidity-route-20260722). Session A falsifies strong rigidity via a balanced quartic; Session B exhibits an honest HamDyn inhabitant of the weak/CanonicalMom schemas and banks a DEFINED-only rigidity statement for later sessions. No ledger flag is flipped: gap5_constraint_recovery stays false.
The model under study is the balanced quartic on a two-site register. Hamiltonian density is the pure quartic kinetic term $\pi_j^4$. The nondegenerate design witness is the phase-space point with zero configuration and momentum $\pi=(1,0)$ (unit load on site 0, zero on site 1). Companion structure and momentum densities are chosen so a balance identity cancels the ham-ham right-hand side on $\mathbb{Z}/2\mathbb{Z}$.
proof idea
Term-mode proof by unfolding. Simplify with the two defining equations: Hamiltonian density is fourth power of the momentum coordinate, and the witness phase has momentum 1 at site 0. The goal reduces to $1^4 \neq 0$, discharged by numeric normalization. No external lemmas are required.
why it matters
Supplies the nondegeneracy witness that the balanced quartic Hamiltonian density is a genuine (nonzero) functional at the design point used for mom_load_bearing. Downstream it feeds the weak point-split inhabitant: the balanced quartic is packaged as an HKTPointSplitTargetDyn 2 with this density, the matching momentum density, structure function, and advector maps. That inhabitant is the Session B separation object between the balanced quartic and the CanonicalMom rigidity route. Within the SevenGaps gravity stack it is bookkeeping for gap5, not a physics constant derivation; it does not touch T5-T8, RCL, or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.