zero_density_fails_nondegenerate
plain-language theorem explainer
Zero density fails nondegeneracy by construction: no two-site phase-space point and Z/2Z index can make 0 ≠ 0. Cited when filtering junk witnesses out of the point-split HKT dynamic target at n=2. Proof is pure existential elimination against reflexivity of real equality.
Claim. There do not exist a point of the two-site phase space and an index $j \in \mathbb{Z}/2\mathbb{Z}$ such that $0 \neq 0$ holds in $\mathbb{R}$.
background
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target. The unsplit momentum–Hamiltonian field is uninhabitable for honest nearest-neighbor local momentum profiles against a frozen quadratic Hamiltonian: at $n=2$, unsplit advection forces a singular identity on $p_0+p_1=0$. The repaired sibling uses a smeared point-split momentum density with source/target advection densities.
Nondegeneracy is the filter that discards trivial density profiles. Zero density is the canonical junk profile: every scalar built from it is the real zero, so any nondegeneracy clause that demands a nonzero real is definitionally false. The ambient phase space is the $n=2$ discrete configuration; indices run over $\mathbb{Z}/2\mathbb{Z}$.
No rigidity theorem is proved in this module. The load-bearing class is the strong point-split target; the weak schema is demoted after the quartic zero-momentum decoy adjudication.
proof idea
Term-style contradiction on an existential. Unpack the assumed witnesses (phase-space point, $\mathbb{Z}/2\mathbb{Z}$ index, and hypothesis $h:0\neq 0$). Discharge by applying $h$ to rfl, since $0=0$. No lemmas from the gravity stack are invoked; the argument is pure equality logic.
why it matters
Closes the zero-density corner of the nondegeneracy filter for the point-split HKT dynamic target after the Wave C2 R5 repair. The module header records that the weak point-split schema is inhabited by a quartic zero-momentum decoy and is demoted; binding rigidity lives in the strong statement. This lemma is the trivial half of that hygiene: zero density cannot pass nondegeneracy, so it never contaminates the strong class.
No downstream consumers are wired yet (used_by is empty). It does not flip any ledger flag and does not touch T5–T8, the Recognition Composition Law, or the $\varphi$-ladder mass formula. Its role is local API hygiene inside the seven-gaps gravity stack: keep junk profiles out before any rigidity claim is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.