unsplitNoGoPhase
plain-language theorem explainer
Concrete two-site phase-space witness used to force the unsplit mom–ham obstruction: configuration $(0,1)$ and momenta $(1,-1)$, giving the local triple $(d,\pi_0,\pi_1)=(1,1,-1)$. Gravity/HKT authors cite it when evaluating brackets and the frozen-Hamiltonian nearest-neighbor no-go on $\mathrm{PhaseSpace}\,2$. It is a pure definitional pair of functions on $\mathbb{Z}/2\mathbb{Z}$.
Claim. Define the phase-space point on the two-site periodic lattice by configuration $q(0)=0$, $q(1)=1$ and conjugate momenta $\pi(0)=1$, $\pi(1)=-1$. This is the no-go witness with local nearest-neighbor data $(d,\pi_0,\pi_1)=(1,1,-1)$.
background
In the hypersurface-deformation model, the canonical phase space on an $n$-site periodic lattice is the product of configuration and conjugate-momentum fields $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, so points are pairs of real values on the two sites.
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target after adjudication: the unsplit mom_ham field is uninhabitable for honest nearest-neighbor local momentum profiles against the frozen quadratic Hamiltonian. At $n=2$, unsplit advection forces $(p_0+p_1)\cdot\partial_d f=p_0^2+d^2$, which is singular on $p_0+p_1=0$.
Local momentum profiles are maps $m_j=f(d_j,\pi_j,\pi_{j+1})$; the witness is chosen so $d=1$, $\pi_0=1$, $\pi_1=-1$ (equivalently $q(1)-q(0)=1$ with those momenta), where the singularity and the forced PDE on partials of $f$ become elementary.
proof idea
Definitional construction, not a proof. The value is the ordered pair of functions on $\mathbb{Z}/2\mathbb{Z}$:
- configuration: $0$ at site $0$, $1$ at site $1$;
- momentum: $1$ at site $0$, $-1$ at site $1$.
The private lemma unsplitNoGo_vals simply unfolds the definition by simp to expose the four coordinate equalities for downstream rewrites.
why it matters
This witness is the concrete point at which the scoped no-go is evaluated. Downstream, unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam shows no Fréchet-smooth nearest-neighbor local momentum profile satisfies the unsplit Dyn mom_ham identity against the frozen quadratic Hamiltonian on $\mathrm{PhaseSpace},2$: at this point with weight $w=\delta_0$, unsplit forces $(N_0+N_1)(-f_d+f_p-f_r)=N_1-N_0$ for all lapses $N$, and the two delta lapses yield an inconsistent linear system on the partials.
Supporting identities bracket_MomFromProfile_delta0_unsplitNoGo and unsplit_RHS_delta0_unsplitNoGo evaluate the momentum–Hamiltonian bracket and the unsplit right-hand side exactly at this point. The module records the unsplit Dyn target as falsification-adjacent; the load-bearing repaired class is the strong point-split target. No rigidity theorem is proved here, and the analogous claim against campaign HamDyn remains an open Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.