calibratedJet_hp_eq_linear
plain-language theorem explainer
Calibration of every site's jet cost forces the log-curvature coefficient to 1, so the Hamiltonian momentum response collapses to κ² p at every field pair. Gravity workers citing the HKT kinetic-normalization reduction use this to discharge the linear-response half of the disclosed premise with cKin = κ²/2. The proof evaluates the calibrated quadratic profile and invokes uniqueness of derivatives.
Claim. Let $h$ be a local Hamiltonian density profile with smooth momentum response $S$, and suppose $h(a,b,p)=\frac{c(a,b)}{2}(\kappa p)^2+U(a,b)$ for continuous $c$, fixed $\kappa$, and link term $U$. If each jet cost $F_c(x)=\frac{c}{2}(\log x)^2$ is calibrated (second derivative of $G(t)=F(e^t)$ at $0$ equals $1$), then $S.hp(a,b,p)=\kappa^2\,p$ for all field values $a,b$ and momentum $p$.
background
This module sits in Pillar 1 of the Seven Gaps gravity program. The ambient target KineticNormalizedCanonicalMom carries a disclosed premise that the momentum response is linear with a field-independent coefficient: $S.hp(a,b,p)=(2,c_{\mathrm{Kin}})p$ with $c_{\mathrm{Kin}}\neq 0$. Four kill theorems show the rigidity conclusion fails without that premise, so the load is real. The module's job is to cut the premise in half and record exactly how far recognition-cost structure can go.
Calibration (Condition 1.2) means $\lim_{t\to 0} 2F(e^t)/t^2=1$, equivalently $G''(0)=1$ for $G(t)=F(e^t)$. The jet family here is $F_c(x)=\frac{c}{2}(\log x)^2$; calibration forces $c=1$ pointwise. The profile is packaged as a map on $\mathbb{R}^3$ via profileMap, and smoothness of that map supplies the derivative of the momentum response used below.
Upstream, channel separation ($h=K(p)+U(a,b)$ with $K$ stationary at zero) is already equivalent to field-independent linear response under the CanonicalMom axioms. The present theorem is the calibrated-jet specialization of that story: once every site is calibrated, the quadratic jet profile yields an explicit constant $c_{\mathrm{Kin}}=\kappa^2/2$.
proof idea
First apply the local calibration equivalence: isCalibrated_jetCost_iff converts $hCal$ into $c(a,b)=1$. Substitute into the profile hypothesis to rewrite $h(a,b,t)=\frac12(\kappa t)^2+U(a,b)$.
Invoke hasDerivAt_hp_of_normalized to obtain a derivative of the momentum response at $(a,b,p)$. On the rewritten profile, differentiate by the chain rule: $\kappa t$ has derivative $\kappa$, its square has derivative $2(\kappa p)\kappa$, and the factor $1/2$ yields $\kappa^2 p$. The constant link $U$ contributes nothing. Uniqueness of derivatives identifies $S.hp(a,b,p)$ with that value; a final ring simplification rewrites $\kappa^2 p$ as $(2\cdot(\kappa^2/2))p$, matching the disclosed linear form.
why it matters
The theorem is the field-independence half of the disclosed kinetic premise, derived rather than assumed, once the density is a calibrated per-site jet. Downstream it feeds the structure CalibratedJetCanonicalMom, whose existence clause packages exactly these hypotheses (smooth profile, nonzero $\kappa$, calibrated jets) as a CanonicalMom target whose momentum sector is a global-chart jet.
It also sits next to jetCost_not_rcl, which shows the jet family violates the Recognition Composition Law for every nonzero curvature (residual $-\frac{c^2}{2}(\log x)^2(\log y)^2$). Calibration alone therefore does not make the object a recognition cost; §8 must impose the composition law separately. In the broader forcing chain this is gravity-side bookkeeping, not T5–T8, but it tightens the load-bearing surface of HKT kinetic rigidity to field-independence of the coefficient, with the linear shape forced by the point-split functional equation already on the CanonicalMom target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.