quarticBalancedStructure2_not_constant
plain-language theorem explainer
The balanced quartic structure 1 + q_j^2 is not constant on two-site phase space. Anyone assembling or citing the weak HKT point-split target for n=2 needs this non-constancy to keep the model out of the frozen-metric class. The proof compares the zero and unit configuration points at one site and reads off 1 ≠ 2 by arithmetic.
Claim. The two-site structure function $(q,\pi,j)\mapsto 1+q_j^2$ is not phase-space constant: there exist canonical points $x,y$ and a lattice site $j$ with $1+q_j(x)^2 \neq 1+q_j(y)^2$.
background
Local setting is Wave C2 gap5 (binding design D-qg-hkt-rigidity-route-20260722): kill strong rigidity and repair the CanonicalMom class for HKT point-split dynamics. Session B exhibits an honest HamDyn inhabitant, separates the balanced quartic, and banks a DEFINED-only CanonicalMom rigidity statement; no ledger flag is flipped.
A lattice inverse-metric candidate is phase-space constant when changing the canonical data cannot change its value at any site. The balanced quartic structure is the model $1+q_j^2$ (same shape as the dynamic structure). Two fixed witnesses on PhaseSpace 2 are used throughout the blocker stack: the zero canonical point (all configurations and momenta zero) and the unit configuration point (all configurations 1, momenta zero).
proof idea
Short contradiction in term mode. Assume the structure is phase-space constant, then instantiate at the zero phase point, the unit configuration point, and site $0\in\mathbb{Z}/2\mathbb{Z}$. Unfold the structure definition and the two points to the numerical claim $1=1+1$, and discharge by norm_num. No external lemmas beyond the three local definitions.
why it matters
Direct input to quarticBalancedWeakTarget, which packages the balanced quartic densities and this structure as an inhabitant of the weak point-split schema for $n=2$. That inhabitant is the Session B witness separating the balanced quartic from rigid inverse-metric candidates while the CanonicalMom rigidity statement remains DEFINED-only for later sessions. Non-constancy is the elementary obstruction preventing $1+q_j^2$ from being a frozen lattice metric, supporting the gap5 route against strong point-split rigidity. The module keeps gap5_constraint_recovery false.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.