perSiteJetProfile
plain-language theorem explainer
Defines the local Hamiltonian density whose kinetic piece is a balance jet of a site-dependent cost, read in one global momentum chart κ: h(a,b,p)=(c(a,b)/2)(κ p)²+U(a,b). Log-curvature c may depend on the neighbouring fields; field-independence is not built in. Downstream calibrated-jet rigidity and ADM shape theorems cite this shape as the ambient class.
Claim. For $c,U:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ and chart scale $\kappa\in\mathbb{R}$, the per-site jet profile is the local Hamiltonian density $h(a,b,p)=\frac{c(a,b)}{2}(\kappa p)^{2}+U(a,b)$ on neighbouring field values $(a,b)$ and momentum $p$.
background
This module sits in Pillar 1 of the Seven Gaps gravity work: reduce the disclosed premise of kinetic-normalized canonical-momentum rigidity. That premise said the momentum response is linear with a field-independent coefficient. Half of it (linearity) is forced by the point-split functional equation once the response vanishes at zero momentum; the remaining load is field-independence alone, equivalently channel separation $h=K(p)+U(a,b)$.
A local Hamiltonian profile assigns a density to a pair of neighbouring field values and a momentum. The recognition cost $J$ has curvature $J''(1)$ at balance; calibration of a one-parameter jet means that curvature matches $J''(1)$. The chart $t=\kappa p$ converts momentum to a log-imbalance coordinate so curvature statements are chart-invariant up to the fixed scale $\kappa\neq 0$.
The formula here packages exactly that jet shape without forcing $c$ constant: each bond $(a,b)$ may carry its own log-curvature $c(a,b)$, plus an arbitrary link term $U$.
proof idea
Pure definitional abbreviation: the profile map is the quadratic form $(c(a,b)/2)(\kappa p)^{2}$ plus $U(a,b)$. No lemmas, no tactics; the body is the closed-form density used by later calibration and rigidity statements.
why it matters
This is the ambient density class for calibrated-jet targets. CalibratedJetCanonicalMom packages a canonical-momentum target whose momentum sector equals some perSiteJetProfile with every site's jet calibrated. From that, calibratedJet_hp_eq_linear derives field-independence: calibration forces every log-curvature to 1, so the momentum response is $\kappa^{2}p$ everywhere (disclosed premise with $c_{\mathrm{Kin}}=\kappa^{2}/2$). calibratedJet_ADM_rigidity then concludes every such target is ADM in shape with the canonical momentum relation, without assuming field-independence up front.
Non-vacuity is witnessed by hamDynCalibratedJet: the ADM anchor is literally this profile with $c\equiv 1$, $\kappa=1$. The variable-kinetic kill inhabitant also fits (vacuumKineticLocalProfile_eq_perSiteJet), so the shape is wide enough to host counterexamples when calibration is dropped. Calibration itself is rephrased as a density-curvature identity via isCalibrated_iff_density_curvature in the chart $t=\kappa p$, matching recognition curvature $J''(1)$. Framework role: close the kinetic half of HKT rigidity toward recognition cost without smuggling field-independence into the hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.