vacuumKinetic_structure_nonconstant
plain-language theorem explainer
The structure function attached to the vacuum-kinetic canonical-momentum target is not phase-space constant: its value can change when the canonical data change. Gravity auditors cite it as an explicit decoy witness that non-constant structure alone does not force ADM shape. The proof is a one-line term application of the dynamic non-constancy lemma for that structure function.
Claim. Let $g$ be the structure function of the vacuum-kinetic canonical-momentum target on phase space. Then $g$ is not phase-space constant: it is not the case that $g(x,j)=g(y,j)$ for all phase-space points $x,y$ and all lattice sites $j$.
background
This module closes Wave C4/C5 gap5 on the HKT side: a mod-vacuum kill together with kinetic-normalized rigidity. The local objects are vacuum-kinetic profiles (amplitude, weight, kinetic density) and a canonical-momentum target whose structure function is a lattice inverse-metric candidate on phase space.
PhaseSpaceConstant means a map $g:\mathrm{PhaseSpace},n\to\mathbb{Z}/n\to\mathbb{R}$ is independent of the phase-space argument: $g,x,j=g,y,j$ for every pair of phase-space points and every site $j$. Equivalently, changing canonical data cannot change the value at any site.
The theorem sits among sibling vacuum-kinetic constructions (vacuumKineticA, W, K, local profile, Hamiltonian density). The doc flags it as a decoy: non-constancy of structure is a counterexample witness, not an ADM-shape forcing step. A companion remark notes that the functional equation collapses to $0=0$ on the diagonal and likewise does not force constant kinetic.
proof idea
One-line term proof: the goal is exactly the negation of PhaseSpaceConstant on vacuumKineticCanonicalMomTarget.structureFunction, and that is the conclusion of structureDyn_not_constant. No extra rewriting or case split; the declaration is a named packaging of that upstream non-constancy fact.
why it matters
In the gap5 HKT program the module must separate genuine rigidity (kinetic-normalized canonical momentum, FTC recovery as a derived theorem) from superficial non-constancy signals. This lemma records that the vacuum-kinetic structure function fails phase-space constancy, so any argument that tried to read ADM shape off "structure is non-constant" is blocked by an explicit witness.
It supports the C4/C5 adjudication path (D-qg-hkt-modvacuum-verdict, D-gap5-acceptance-adjudication): Part 1 kills mod-vacuum rigidity via a variable-kinetic CanonicalMom inhabitant; Part 2 owns kinetic-normalized intensivity with theorem-derived FTC recovery. No downstream consumers are wired yet; the declaration is a terminal decoy marker inside the SevenGaps gravity stack rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.