unitStructure_is_phaseSpaceConstant
plain-language theorem explainer
The constant unit inverse-metric weight on the lattice phase space is phase-space constant: its value at every site is independent of the canonical data. Gravity workers comparing frozen HKT structure against the widened dynamic-structure target cite this as the baseline witness. The proof is a two-line introduction plus reflexivity.
Claim. The map sending every phase-space point $(q,\pi)\in(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/n\mathbb{Z}\to\mathbb{R})$ and every lattice site $j$ to the real number $1$ is phase-space constant: its value does not depend on the choice of canonical data.
background
In the lattice hypersurface-deformation setting, the canonical phase space at $n$ sites is the product of configuration and conjugate momentum, each a real function on the periodic lattice $\mathbb{Z}/n\mathbb{Z}$. A candidate inverse-metric weight is a real-valued function of that phase space and a site index.
Phase-space constancy means the weight is blind to the canonical data: changing $(q,\pi)$ cannot change the value at any site. The module widens the classical Hojman–Kuchař–Teitelboim (HKT) target so that a structure function may vary; the frozen unit weight $g\equiv 1$ is the baseline against which nonconstant structure is measured.
Codex adjudication rejected folding a dynamical $g$ into momentum density while still selling frozen unit structure as GR. This lemma records that the constant-$1$ weight sits inside the phase-space-constant class used by the dynamic-structure blocker.
proof idea
Unfold phase-space constancy and introduce arbitrary phase-space points $x,y$ and site $j$. Both sides of the required equality are definitionally $1$, so reflexivity closes the goal. No lemmas are invoked.
why it matters
Inside the SevenGaps gravity stack this pins the frozen unit structure as a legitimate phase-space-constant witness for the widened HKT dynamic target (Wave C2 R5/R6 groundwork). Downstream rigidity and status flags in the same module compare dynamic structure functions against this baseline; without it the constant slot would be informal.
The original one-site HKT rigidity statement is already known false; the dynamic target keeps an explicit structure-function slot with a nonconstancy side condition. Establishing that unit structure is phase-space constant separates the frozen GR-like case from genuinely dynamical structure, and supports later no-go results on unsplit momentum–Hamiltonian constraints for nearest-neighbor profiles against frozen quadratic Hamiltonians.
No parent theorem currently depends on this declaration in the graph; it is groundwork for the dynamic HKT status bundle rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.