not_HKTRigidityStatementPointSplitDynN2Strong
plain-language theorem explainer
Strong-class HKT rigidity at dynamical point-split n=2 is false. Anyone tracking Gap 5 (the HKT rigidity route) cites this as the kill of the unconditioned strong statement. The balanced quartic strong target forces p^4 = c_kin p^2 + c_vac at three momenta after the gradient term drops, and those three equations are inconsistent.
Claim. The strong dynamical point-split HKT rigidity statement at $n=2$ is false: it is not the case that every strong $n=2$ target has Hamiltonian density of the form $c_{\mathrm{kin}}\,\pi^2 + c_{\mathrm{grad}}(\nabla q)^2 + c_{\mathrm{vac}}$ with universal coefficients. The balanced quartic supplies a counterexample.
background
Gap 5 in the Seven Gaps gravity stack concerns whether Hamilton–Killing–type (HKT) targets on a point-split dynamical lattice are rigid: whether the local energy density is forced into a fixed quadratic kinetic plus gradient plus vacuum shape. The strong class HKTPointSplitTargetDynStrong 2 tightens the weak target by balance and density constraints; the associated rigidity statement asserts that every such strong target is of that three-coefficient form.
Session A of this module inhabits the strong class by the balanced quartic (Hamiltonian density $\sim p^4$ with a balanced structure profile on $\mathbb{Z}/2\mathbb{Z}$ phases) and then kills the rigidity claim. The local setting is binding design D-qg-hkt-rigidity-route: kill unconditioned strong rigidity, then repair the target class with a canonical-momentum density field before any ledger flag flips.
Constant configurations (vanishing spatial gradient) reduce the putative rigid form to $p^4 = c_{\mathrm{kin}} p^2 + c_{\mathrm{vac}}$, which is already overconstrained once three momenta are plugged in.
proof idea
Assume the strong rigidity statement. Instantiate it on the balanced quartic strong target to obtain coefficients $c_{\mathrm{kin}}, c_{\mathrm{grad}}, c_{\mathrm{vac}}$ and a form identity for every configuration and phase.
Restrict to constant configurations at phase $0$ with free momentum $p$. The gradient density vanishes; unfolding the strong/weak target densities and the $\mathbb{Z}/2$ successor lemmas yields $p^4 = c_{\mathrm{kin}} p^2 + c_{\mathrm{vac}}$. Specialize at $p = 0,1,2$:
- $0 = c_{\mathrm{vac}}$
- $1 = c_{\mathrm{kin}} + c_{\mathrm{vac}}$
- $16 = 4 c_{\mathrm{kin}} + c_{\mathrm{vac}}$
norm_num then linarith closes the contradiction. No external named lemmas beyond the local density unfoldings and $\mathbb{Z}/2$ arithmetic are required.
why it matters
This is the first kill in the Gap 5 tower. Downstream, gap5_kill_tower_scope_certificate packages it with three sibling non-rigidity theorems as a scope certificate that stronger unconditioned $n=2$ rigidity statements are false. The status flag theorem sets rigidityStrongKilled = true while leaving gap5_constraint_recovery false and canonical-momentum rigidity open for Sessions B–C.
It also feeds the discrimination receipt that the honest strong inhabitant is nonempty while the zero-momentum decoy fails the strong class. In the Recognition gravity program this clears a false rigidity route before the repaired CanonicalMom class (local Hamiltonian profile, structure profile $g(q_j)$, and nonzero canonical momentum density $m_j = c_{\mathrm{Mom}}\pi_{j+1}(q_{j+1}-q_j)$) is installed. No forcing-chain landmark (T5–T8) is discharged here; the result is purely a negative constraint on the HKT target hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.