quarticBalancedLoadPhase
plain-language theorem explainer
A concrete two-site phase-space point with configuration and momentum both equal to the Kronecker spike at site 0, written (q,π)=((1,0),(1,0)). Gravity workers cite it as the design witness that the balanced-quartic momentum observables are load-bearing. The body is a pure pair of indicator functions on Z/2Z; no proof obligations.
Claim. Let the two-site lattice phase space be pairs $(q,\pi)$ of real functions on $\mathbb{Z}/2\mathbb{Z}$. Define the load-bearing witness point by $q(0)=1$, $q(1)=0$ and $\pi(0)=1$, $\pi(1)=0$.
background
In the hypersurface-deformation model, the canonical phase space on an $n$-site periodic lattice is the product of configuration and conjugate momentum: pairs of maps $\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Coordinate functionals and Poisson brackets are built from that product structure.
This module closes Wave C2 gap5 on the HKT point-split route: Session A falsifies strong rigidity at $n=2$ with a balanced quartic; Session B separates an honest Hamiltonian dynamics inhabitant and banks a DEFINED-only canonical-momentum rigidity statement. No ledger flag is flipped.
The present definition supplies one fixed phase-space point used to test whether momentum observables actually move under the Poisson bracket (the load-bearing condition).
proof idea
Definitional construction only. Both components are the same indicator on $\mathbb{Z}/2\mathbb{Z}$: value $1$ at residue $0$ and $0$ at residue $1$. No lemmas are applied; the pair is the term.
why it matters
Feeds the load-bearing witness theorem, which shows the Poisson bracket of the two balanced momentum densities is nonzero at this point, and the strengthened target inhabitant that packages honest advection, load-bearing momentum, and kinetic regularity for the balanced quartic at $n=2$.
That inhabitant is the concrete counterexample separating the strengthened dynamical class from naive rigidity, while the repaired canonical-momentum class remains DEFINED-only for later sessions. It sits inside the gravity seven-gaps program (binding design D-qg-hkt-rigidity-route), not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.