quarticHamDensity2_nondeg
plain-language theorem explainer
The quartic Hamiltonian density at the designated non-degenerate phase is nonzero on site 0 of Z/2Z. Gravity auditors cite it when building the quartic zero-momentum decoy that inhabits the weak HKT point-split schema. The proof unfolds the density and phase definitions, then closes by numeric normalization.
Claim. Let $\rho$ be the quartic Hamiltonian density on the two-site lattice and let $\theta_*$ be the designated non-degenerate phase. Then $\rho(\theta_*, 0) \neq 0$ for $0 \in \mathbb{Z}/2\mathbb{Z}$.
background
Module setting is Wave C2 repair of the HKT point-split target after the adversarial pass that found the weak dynamical schema decoy-inhabitable. The weak class only asks for a Hamiltonian density, a momentum density, a structure function, and advection maps; it does not force load-bearing momentum or Mom–Ham bracket calculus.
The quartic density is the explicit decoy Hamiltonian used with vanishing momentum. Non-degeneracy at a fixed phase and at site 0 guarantees the density is not the zero functional, so the decoy is a genuine (if pathological) inhabitant rather than a vacuous zero map. Spatial dimension $D=3$ and the eight-tick period sit upstream in the forcing chain but are not invoked in this local numeric check.
proof idea
Term-mode proof: unfold the quartic density and the non-degenerate phase definitions with simp only, then discharge the resulting concrete rational inequality by norm_num. No external lemmas are required beyond definitional reduction.
why it matters
Feeds quarticZeroMomTarget, the formal witness that the weak point-split dynamical schema is decoy-inhabitable (adjudication note D-qg-hkt-pointsplit-adjudication-20260722). That witness is why the module strengthens the target: load-bearing momentum, advection tied to the Mom–Ham bracket, and kinetic regularity exclude the quartic zero-momentum decoy while still admitting the honest Hamiltonian inhabitant.
In the broader SevenGaps gravity stack this is diagnostic scaffolding, not a physics claim: it records that weak-class rigidity is not load-bearing and pushes binding rigidity work to the canonical-momentum target. It does not touch T5–T8 forcing, RCL, or the alpha band; it only polices the HKT point-split discrimination gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.