hamDynNondegPhase
plain-language theorem explainer
Concrete nondegenerate phase-space point on the two-site lattice: vanishing configuration and unit momentum supported only at site 0. Gravity and HKT-target authors cite it as the standard witness that HamDyn density and its kinetic sector are nonzero. The body is pure data: a pair of functions on Z/2Z.
Claim. The phase-space point $(q,\pi)\in(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$ with $q_i=0$ for every site $i$ and $\pi_j=1$ if $j=0$, else $\pi_j=0$.
background
Phase space on the periodic lattice with $n$ sites is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, so sites are just the two elements of $\mathbb{Z}/2\mathbb{Z}$.
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target. The unsplit momentum–Hamiltonian field is uninhabitable for honest nearest-neighbor local momentum against the frozen quadratic Hamiltonian: at $n=2$ unsplit advection forces a singular identity on $p_0+p_1=0$. The repaired API uses smeared point-split momentum densities with source/target advection slots; the momentum sector is non-abelian (Wronskian density, not zero).
No rigidity theorem is claimed in the module. The load-bearing class is the strengthened point-split target; the weak schema remains after adjudication.
proof idea
Definitional construction, not a proof. The value is the ordered pair whose first component is the zero configuration on $\mathbb{Z}/2\mathbb{Z}$ and whose second component is the indicator of site $0$ (value $1$ at $0$, value $0$ at $1$). No lemmas are applied.
why it matters
Supplies the standard nondegeneracy witness for the HamDyn sector of the repaired point-split HKT target. Downstream, hamDynDensity_nondeg evaluates the dynamic Hamiltonian density at this point and site $0$ and obtains a nonzero real; hamDyn_kinetic_regular_witness shows the partial derivative of the smeared HamDyn functional in the momentum direction at site $0$ is nonzero on this point. Both feed the honest HamDyn inhabitant of the (weak and strong) point-split targets and the vacuum-shift variants that reuse the same momentum sector.
In the SevenGaps gravity campaign this closes the concrete inhabitability side of the Wave C2 R5 repair: the unsplit Dyn target stays as a falsification-adjacent record, while this phase point lets the point-split strong target carry a genuine kinetic load. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it is local lattice kinematics for the HKT bracket algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.