quarticBalancedNondegPhase
plain-language theorem explainer
A concrete two-site phase-space point with vanishing configuration and momentum supported only at site 0: q ≡ 0, π = (1,0). Gravity and HKT-rigidity work cite it as the nondegeneracy and kinetic-regularity witness for the balanced quartic Hamiltonian density. The body is a pure pair of functions, no proof.
Claim. Let the two-site phase space be pairs $(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. Define the point with $q_j=0$ for all sites and $\pi_0=1$, $\pi_1=0$.
background
In the hypersurface-deformation setup, the canonical phase space of the lattice wave field is the product of configuration and conjugate momentum on a periodic lattice of $n$ sites: $(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$.
This module (Wave C2, gap5) builds the balanced-quartic inhabitant of the point-split dynamical targets, both weak and strengthened, in order to separate honest Hamiltonian dynamics from strong rigidity claims. The balanced quartic supplies Hamiltonian and momentum densities, structure functions, and advection slots on that two-site lattice.
The present declaration is simply one fixed phase-space point used as a numerical probe: zero field, unit momentum on the first site.
proof idea
Definition only: the value is the ordered pair of maps $(q,\pi)$ with $q$ the zero function on $\mathbb{Z}/2\mathbb{Z}$ and $\pi$ the indicator of site $0$ (value $1$ at $0$, value $0$ at $1$). No lemmas or tactics.
why it matters
Downstream nondegeneracy and regularity theorems evaluate the balanced-quartic Hamiltonian density and its momentum derivative at this point: they show the density at site $0$ is nonzero and that the partial derivative of the total Hamiltonian in the $\pi_0$ direction is nonzero. Those facts feed the weak point-split target (ham/mom densities and advection) and the strengthened target (load-bearing momentum plus kinetic regularity).
In the gap5 binding design this is the concrete witness that the balanced quartic is an honest dynamical inhabitant rather than a degenerate shell, supporting the route that kills strong rigidity for $N=2$ while leaving the ledger flag gap5_constraint_recovery false. It is scaffolding for the CanonicalMom class repair, not a physics law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.