coincidentPhaseKin
plain-language theorem explainer
Builds the constant two-site phase-space point where every lattice site carries the same configuration value q and the same conjugate momentum p. Downstream rigidity-kill arguments evaluate Hamiltonian densities at this locus to force coefficient identities. The body is a pure pair of constant maps on ZMod 2; no proof content.
Claim. For $q,p\in\mathbb{R}$, the coincident phase-space point is the pair of constant maps $(i\mapsto q,\, i\mapsto p)$ in the two-site phase space $(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$.
background
The ambient phase space on an $n$-site periodic lattice is the product of configuration and conjugate-momentum fields: pairs $(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, the minimal even lattice used throughout the HKT gap-5 arguments.
This module closes Wave C4/C5 gap5: a mod-vacuum kill of CanonicalMom rigidity via a variable-kinetic inhabitant, followed by the kinetic-normalized rigidity terminal. The variable-kinetic density is already packaged as a CanonicalMom target; evaluations at special phase-space points extract the kinetic, gradient, and momentum coefficients.
The name "coincident" means both sites share identical $(q,p)$ values, so site-dependent structure collapses and density identities become pure algebraic constraints on those coefficients.
proof idea
Definitional construction only: return the pair of constant functions fun _ => q and fun _ => p at type PhaseSpace 2. No lemmas, no tactics.
why it matters
Supplies the evaluation locus for the mod-vacuum rigidity kill. The parent theorem not_HKTRigidityModVacuumStatementN2 assumes an arbitrary mod-vacuum CanonicalMom rigidity witness against the variable-kinetic target, then specializes the Hamiltonian-density identity at coincident points (q,p) to force contradictory coefficient relations. The companion lemma vacuumKinetic_fails_modVacuum_hamShape likewise uses these points to show the variable-kinetic density refuses the rigid mod-vacuum ham-density shape.
Together these close Part 1 of the module binding (D-qg-hkt-modvacuum-verdict): mod-vacuum CanonicalMom rigidity is false on $N=2$. That frees the kinetic-normalized intensivity path (Part 2) without assuming FTC recovery as a class field. No direct T0–T8 landmark; this is gravity-side gap-5 ledger work inside the SevenGaps stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.