HKTRigidityKineticNormalizedN2
plain-language theorem explainer
Terminal proposition: every kinetic-normalized CanonicalMom target on the n=2 lattice has ADM-shaped Hamiltonian density (ultralocal kinetic plus structure-weighted gradient plus local potential) and standard momentum density, with c_mom = 4 c_kin c_grad. Gap5 Hojman/GR-pin ledger and the holds theorem cite it. Pure Prop definition encoding the rigidity claim.
Claim. Every kinetic-normalized CanonicalMom target $T$ admits constants $c_{\mathrm{kin}}\neq 0$, $c_{\mathrm{grad}}\neq 0$, $c_{\mathrm{mom}}=4\,c_{\mathrm{kin}}c_{\mathrm{grad}}$ and a potential $V:\mathbb{R}\to\mathbb{R}$ such that on phase space $(\mathrm{Z}/2\mathrm{Z}\to\mathbb{R})^2$, the Hamiltonian density equals $c_{\mathrm{kin}}\pi_j^2 + c_{\mathrm{grad}} S_j(\Delta q_j)^2 + V(q_j)$ and the momentum density equals $c_{\mathrm{mom}}\pi_{j+1}\Delta q_j$.
background
Module Wave C4/C5 closes gap5 in two halves: kill mod-vacuum rigidity by a variable-kinetic CanonicalMom counterexample, then prove rigidity inside the kinetic-normalized subclass. Binding notes are D-qg-hkt-modvacuum-verdict-20260723 and the C5 upgrade D-gap5-acceptance-adjudication-20260723.
KineticNormalizedCanonicalMom packages an HKT point-split CanonicalMom target together with ultralocal intensivity normalization: there exist a local Hamiltonian profile, ContDiff-2 smoothness, and $c_{\mathrm{kin}}\neq 0$ with intensivity $h_p=2 c_{\mathrm{kin}} p$. The former assumed FTC-recovery field is discharged as the derived theorem ftc_recovery_of_normalized.
Phase space at $n=2$ is the product of configuration $q:\mathrm{Z}/2\mathrm{Z}\to\mathbb{R}$ and conjugate momentum $\pi$ on the two-site periodic lattice. Hamiltonian and momentum densities are the point-split target fields; the structure function $S$ weights nearest-neighbor gradients.
proof idea
Definitional Prop, not a proved theorem. It quantifies over every KineticNormalizedCanonicalMom inhabitant $T$ and asserts existence of three real coefficients and a unary potential $V$ such that: (i) $c_{\mathrm{kin}}$ and $c_{\mathrm{grad}}$ are nonzero with the Hojman relation $c_{\mathrm{mom}}=4 c_{\mathrm{kin}} c_{\mathrm{grad}}$; (ii) hamDensity matches the ADM vacuum profile (quadratic kinetic in $\pi_j$, structure-weighted squared nearest-neighbor $\Delta q$, plus $V(q_j)$); (iii) momDensity is the standard bilinear $c_{\mathrm{mom}}\pi_{j+1}\Delta q_j$. The actual proof that the Prop holds is the separate theorem HKTRigidityKineticNormalizedN2_holds, which unpacks ftc_recovery_of_normalized and sets $c_{\mathrm{grad}}:=c_{\mathrm{mom}}/(4 c_{\mathrm{kin}})$.
why it matters
This is the terminal shape claim for the kinetic-normalized half of gap5. Downstream, hojman_pins_general_relativity is literally defined as this Prop; the ledger doc warns that the name overclaims: what is proved is ADM-shape rigidity on an $n=2$ lattice point-split target, not continuum GR. HKTRigidityKineticNormalizedN2_holds inhabits the Prop, and hktKineticNormalizedRigidityStatus_flags flips the gap5 constraint-recovery and kinetic-normalized-closed bits once both ledger halves bind green.
In the Recognition gravity program this is the Hojman-style pin: after mod-vacuum is killed, intensivity plus ContDiff-2 forces the ADM kinetic/gradient/potential split with the classical coefficient relation. Continuum GR remains open via dirac_algebra_continuum_limit; no continuum limit is taken here. Framework-wise it sits in the SevenGaps gravity stack rather than the T0–T8 forcing chain, but it is the discrete rigidity step that would feed any later continuum identification of the recognition Hamiltonian with Einstein–Hilbert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.