HKTRigidityStatementPointSplitDynN2Strong
plain-language theorem explainer
The proposition asserts that every strengthened two-site point-split HKT target has Hamiltonian density of the rigid GR form c_Kin p² + c_Grad S (Δq)² + c_Vac. Gravity and continuum-limit workers would cite it as the former strong-class grind target. It is only a Prop definition; the claim itself is already refuted by the balanced-quartic inhabitant.
Claim. Every strengthened two-site point-split Hamilton–Kirchhoff–Toda target $T$ admits real constants $c_{\mathrm{Kin}}$, $c_{\mathrm{Grad}}$, $c_{\mathrm{Vac}}$ such that for all phase-space points $x$ and sites $j\in\mathbb{Z}/2\mathbb{Z}$, the Hamiltonian density equals $c_{\mathrm{Kin}}\,p_j^2 + c_{\mathrm{Grad}}\,S_T(x,j)\,(\Delta q_j)^2 + c_{\mathrm{Vac}}$, where $p_j=x_2(j)$, $\Delta q_j=q_{j+1}-q_j$, and $S_T$ is $T$'s structure function.
background
Wave C2 of the Seven Gaps gravity program repairs the point-split HKT target after an adversarial pass showed the weak dynamic schema is decoy-inhabitable by a quartic zero-momentum density. The strengthened structure adds three constraints: load-bearing momentum (a nontrivial ${M,M}$ Poisson bracket), advection slots forced equal to Mom–Ham bracket-calculus extractions, and kinetic regularity (some smeared-Ham momentum partial nonzero).
The local setting is discrete two-site phase space with coordinates $(q,p):\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. Advection equalities under the weak split axiom are already proved as hamAdvFrom_eq_computed and hamAdvTo_eq_computed. Honest dynamical density witnesses supply the load-bearing and kinetic-regularity certificates that place the honest target in the strong class while excluding the zero-momentum decoy.
This definition packages the GR-strength rigidity claim over that strong class at $n=2$: every such target would have density exactly quadratic kinetic plus structure-weighted discrete gradient plus vacuum constant.
proof idea
No proof: the declaration is a bare Prop abbreviation. The body is the universal quantification over strong targets of existence of three real coefficients making the density identity hold pointwise on phase space and sites. Downstream, the negation is proved by feeding the balanced-quartic strong inhabitant into the Prop and obtaining $p^4=c_{\mathrm{Kin}}p^2+c_{\mathrm{Vac}}$ at three momenta after the gradient term vanishes on constant configurations.
why it matters
This is the former binding GR-strength rigidity target for Gap 5 point-split HKT work. The module doc records it as PROVEN FALSE; binding rigidity moves to the CanonicalMom class. Downstream, not_HKTRigidityStatementPointSplitDynN2Strong kills it via the balanced quartic, and gap5_kill_tower_scope_certificate packages that negation with three sibling not-theorems as the kill-tower scope certificate for unconditioned $n=2$ rigidity.
In the Recognition gravity stack this closes a decoy route rather than advancing continuum GR recovery: strong-class rigidity without the canonical-momentum filter is dead. The honest dynamical inhabitant still sits in the strong class, so the discrimination gate (honest passes, zero-momentum decoy fails) remains intact; only the universal rigidity claim over the whole strong class fails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.