structureDyn_not_constant
plain-language theorem explainer
The candidate inverse-metric density 1 + q_j^{2} on two-site phase space is not constant under changes of canonical data. Anyone building or citing an HKT point-split Dyn target that uses this structure function needs the non-constancy fact. The proof is a two-point evaluation: zero configuration versus unit configuration yields 1 versus 2.
Claim. The map $(q,p,j)\mapsto 1+q_j^2$ on two-site phase space is not phase-space constant: there exist canonical points $x,y$ and a site $j\in\mathbb{Z}/2\mathbb{Z}$ with $1+q_j(x)^2\neq 1+q_j(y)^2$.
background
This module repairs the Hojman–Kuchař–Teitelboim dynamic target after the unsplit momentum–Hamiltonian bracket proved uninhabitable for smooth nearest-neighbor momentum against a frozen quadratic Hamiltonian at $n=2$. The repaired schema uses a smeared point-split momentum density and a structure function playing the role of a lattice inverse metric.
Phase-space constancy means the structure function is insensitive to the canonical data: its value at every site is the same for every pair of phase-space points. The concrete structure function here is $1+q_j^2$. Two witness points are the zero canonical point (vanishing configuration and momentum) and the unit-configuration point (configuration identically 1, momentum zero).
The local setting is Wave C2 R5: no rigidity theorem is claimed in this file; the structure function is only required to be a well-defined, non-constant density feeding honest HamDyn and vacuum-sector targets.
proof idea
Term-mode proof by contradiction. Assume phase-space constancy of $1+q_j^2$. Instantiate the universal quantifiers 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$, the right side is $1+1^2=2$. norm_num closes the numerical contradiction.
why it matters
Non-constancy is the minimal sanity check that the structure function can carry genuine metric degrees of freedom rather than a frozen background weight. Downstream it is reused verbatim as vacuumKinetic_structure_nonconstant (a decoy showing that structure non-constancy alone does not force ADM shape), and it is the structure field of three concrete targets: the honest HamDyn point-split inhabitant, the vacuum-kinetic weak target, and the vacuum-shift weak target.
In the Seven Gaps gravity campaign this sits inside the HKT dynamic-bracket repair path, not the T0–T8 forcing chain. It does not flip any ledger flag and does not close the open unsplit HamDyn obstruction Prop; it only certifies that the repaired structure density varies on phase space so later rigidity and vacuum-sector arguments have a non-trivial metric sector to work with.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.