powerGeneratedNativeCost_zero_calibrated
plain-language theorem explainer
For every nonzero natural exponent, the native cost generated by that power has doubled-trace zero calibration. Even- and odd-power structural-ledger theorems cite this as the zero-calibration conjunct. The proof reduces the predicate to rational equality of ratio-orbit displays, evaluates via the orbit arithmetic lemmas, then uses 0^n=0 and a numeric check on the J-cost.
Claim. For every natural number $n \neq 0$, the doubled-trace display of the native cost generated by the $n$-th power satisfies zero calibration: its doubled-trace value is cross-equal (equivalently, equal as a rational) to the zero ratio-orbit.
background
In the Primitive Recognition Calculus native-cost ledger, costs are tracked by ratio-orbit displays: a signed-orbit numerator over a nonzero distinction-nat denominator, with a verifier map toRat into $\mathbb{Q}$. Cross-equality of two displays is equivalent to equality of those rationals (K4.10).
The doubled-trace zero-calibration predicate asserts that the doubled-trace value of a native cost matches the zero orbit under that cross-equality. The underlying cost is the power-generated native cost at exponent $n$, whose rational display is computed from the closed-form J-cost $J(x)=(x+x^{-1})/2-1$ (here written jq on ratio orbits).
Upstream arithmetic is the standard ratio-orbit ring: addition, multiplication, and the constants $0,1,2$ all commute with toRat. The local module packages structural certificates that power families satisfy (or almost satisfy) the native-cost hypothesis bundle without leaning on a separate two-calibration axiom.
proof idea
Tactic proof. Unfold zero-calibration to cross-equality, then rewrite by crossEq_iff_toRat_eq to a rational identity. Simplify the doubled-trace display through nativeCostDoubledTrace, doubledTraceValue, and the ratio-orbit lemmas mul_toRat, add_toRat, one_toRat, zero_toRat, together with two_toRat and powerGeneratedNativeCost_toRat. The remaining power of zero is killed by zero_pow using $n\neq 0$. Finish with norm_num on the J-cost display jq, which evaluates the calibrated identity to a trivial numeric fact.
why it matters
This is the zero-calibration leg for every nonzero power-generated native cost. Downstream, the even-power theorem packages base hypotheses, monotonicity, and this calibration while excluding only sign-reversal ("everything except orientation"), and the odd-power theorem uses the sibling base/sign/monotone facts under an anchor-free structural bundle. Together they isolate which ledger fields fail for which parity, rather than treating the power family as an opaque black box.
In the broader Recognition stack this sits under the J-cost calculus forced at T5 ($J(x)=\cosh(\log x)-1$), specialized to the discrete native-cost ledger that later feeds mass and spectrum bookkeeping. It does not itself force $\varphi$ or the eight-tick structure; it only certifies that power-generated costs sit at the calibrated zero of the doubled trace once the exponent is nonzero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.