decorativeStructure2_not_constant
plain-language theorem explainer
The decorative inverse-metric candidate on two-site phase space is not phase-space constant: its value depends on the configuration coordinate. Gravity and HKT-target authors cite it when assembling the quartic zero-momentum decoy that inhabits the weak point-split schema. The proof evaluates the candidate at the zero and unit configuration points and obtains 1 ≠ 2 by arithmetic.
Claim. The map $g(x,j) = 1 + q_j(x)^2$ on two-site phase space is not phase-space constant: there exist canonical points $x,y$ and a site $j$ with $g(x,j) \neq g(y,j)$.
background
This module strengthens the point-split HKT target after an adversarial pass showed the weak dynamical schema is decoy-inhabitable by a quartic zero-momentum package. The discrimination gate requires an honest inhabitant of the strong class and an explicit weak-class decoy excluded by momentum load-bearing.
A lattice inverse metric $g$ is phase-space constant when its value at every site is independent of the canonical data: $g(x,j)=g(y,j)$ for all phase-space points $x,y$ and sites $j$. The decorative structure used here is $g(x,j)=1+q_j(x)^2$, the same algebraic shape as the dynamical structure function but treated as a fixed candidate. Two witness points are the zero canonical point (vanishing configuration and momentum) and the unit-configuration point (configuration one, momentum zero).
proof idea
Assume for contradiction that the decorative structure is phase-space constant. Instantiate the universal quantification at the zero phase point, the unit configuration point, and site $0 \in \mathbb{Z}/2\mathbb{Z}$. Unfold the three definitions: the left side is $1+0^2=1$ and the right side is $1+1^2=2$. norm_num closes the contradiction $1=2$.
why it matters
The lemma feeds quarticZeroMomTarget, the explicit weak-schema inhabitant that witnesses the critic finding: the weak point-split HKT target is decoy-inhabitable by a quartic Hamiltonian density with vanishing momentum, zero advection, and this nonconstant decorative structure. Nonconstancy keeps the decoy from collapsing into a trivial constant-metric package while still failing the strong-class momentum load-bearing gate.
In the SevenGaps gravity line this is bookkeeping for the Wave C2 repair, not a physics derivation of $G$ or the phi-ladder. Strong-class rigidity is already recorded as false via the balanced-quartic falsifier; binding rigidity moves to the canonical-momentum target. No ledger flag is flipped here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.