isCalibrated_powCost_iff
plain-language theorem explainer
Among the one-parameter family F_n(x)=J(x^n) of Recognition Composition Law solutions, exactly the member n=1 is calibrated. Calibration is the missing clause that collapses the family back to J; anyone arguing uniqueness of the recognition cost under RCL plus normalization cites this. The proof reduces calibration to the identity n²=1 on the second derivative of G_F at 0, then finishes by nlinarith on naturals.
Claim. For every natural number $n$, the power-reparametrized cost $F_n(x)=J(x^n)$ is calibrated in the sense that $G''(0)=1$ where $G(t)=F_n(e^t)$ (equivalently $\lim_{t\to 0} 2 F_n(e^t)/t^2=1$) if and only if $n=1$.
background
This module runs the reparametrization attack on the constraint-sector kinetic-weight argument of HKTKineticFromRecognitionCost §8. The Recognition Composition Law (RCL) is quadratic in the cost functional, so it does not pin a unique F: substituting $x\mapsto x^n$ carries solutions to solutions. The resulting family is powCost n, i.e. $F_n(x)=J(x^n)$, each a strictly increasing reparametrization of J on $[1,\infty)$ via Chebyshev polynomials, and $F_n\neq J$ for $n\ge 2$.
Calibration (Condition 1.2) is the missing normalization: writing $G(t)=F(e^t)$, one requires $G''(0)=1$, or equivalently $\lim_{t\to 0} 2F(e^t)/t^2=1$. Upstream, IsCalibrated is exactly that second-derivative statement. The classical J-cost of T5 is the unique calibrated solution of the RCL; this theorem records that fact inside the power orbit.
Locally the point is severity: §8's unit-weight conclusion never inspects the recognition cost itself (only that some F obeying the law is nonzero somewhere), so the attack lands, but calibration still singles out J among the power family.
proof idea
Tactic proof, two directions after unfolding. Rewrite IsCalibrated and apply the computation deriv2_G_powCost, which evaluates $G''(0)$ for $F_n$ as $n^2$ (in real cast). Forward: the calibration hypothesis becomes $(n:\mathbb{R})^2=1^2$; nlinarith with nonnegativity of $(n-1)^2$, $(n+1)^2$, and of $n$ itself forces $n=1$, then cast back to $\mathbb{N}$. Reverse: substitute $n=1$ and close by norm_num (recovering the known calibration of J).
why it matters
Doc-comment clause: the composition law leaves a one-parameter family; calibration is what collapses it to J, and this is precisely the clause §8 does not impose. Downstream, constraint_sector_recognition_load_is_quadraticity_not_unit_weight_holds packages the attack: RCL forces unit weight for any nonzero F (quadraticity of the law), yet powCost still satisfies the law and differs from J at n=2. This theorem supplies the calibration half of that ledger: only n=1 is calibrated, so the recognition load of the constraint sector is the quadratic structure of RCL, not a privileged unit weight tied to J alone.
In the broader forcing chain this is the local face of T5 J-uniqueness inside the gravity/constraint-sector campaign: RCL plus the second-derivative normalization recovers J, while RCL alone does not. It also feeds chart work in Gap5ChartFromLedgerMomentum, where the second power cost is the nearest neighbour of J in the family and the log-chart identities (sinh/arsinh imbalance coordinates) are checked against that neighbour. Campaign 1's invariance test is thereby answered for Gap 5 at lower severity than O5: the orbit stays inside the law, and calibration is the cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.