signedPowerNativeCost_zero_calibrated
plain-language theorem explainer
For every nonnegative integer exponent m, the native cost built from the sign-extended power character has a zero-calibrated doubled trace. Ledger assemblers for anchor-free power characters cite this as one structural field. The proof transports the calibration identity to rationals via toRat lemmas and closes by numeric simplification at the zero argument of the signed power.
Claim. For every natural number $m$, the doubled-trace presentation of the native cost induced by the sign-extended power character $\chi(x)=\mathrm{sgn}(x)\,|x|^{m+1}$ is zero-calibrated (its doubled-trace value meets the PRC zero-calibration identity).
background
In the gauge-orbit cost module, native costs are maps on ratio orbits that record a recognition cost. The sign-extended power native cost for exponent $m$ is generated by $\chi(x)=\mathrm{sgn}(x),|x|^{m+1}$: on a ratio orbit $q$ it returns the zero orbit when $q$ is the unit ratio, and otherwise the orbit of the signed power of the underlying rational.
The Primitive Recognition Calculus structural ledger packages several fields a native cost must satisfy without an external anchor. Zero calibration of the doubled trace is one of those fields: after forming the doubled-trace presentation of the cost, a fixed cross-equality (equivalently, equality after transport to $\mathbb{Q}$) must hold at the calibrated zero.
Upstream, the toRat identity for this cost states that its rational value is $j_q$ of the signed power of the input rational, and the signed power vanishes at argument $0$. Those two facts feed the calibration check directly.
proof idea
Tactic proof, not a bare wrapper. Unfold the zero-calibration predicate and replace the cross-equality by rational equality via crossEq_iff_toRat_eq. Then simplify the doubled-trace presentation using the definitions of native doubled trace and doubled-trace value, the ring morphisms mul_toRat/add_toRat, the constants two and one as rationals, the toRat formula for the signed-power native cost, zero as a rational, and signedPow_zero_arg. Finish with norm_num on the $j_q$ expression, which evaluates to the calibrated zero.
why it matters
This discharges the zero_calibrated field of the anchor-free structural package for every nonnegative integer power character. The immediate parent is signedPowerNativeCost_sansAnchor, whose doc-comment states that every such exponent inhabits the anchor-free ledger, including orientation reversal, at both parities of exponent.
In the Recognition cost hierarchy, power characters are the real-character orbit that must sit inside the PRC native-cost ledger before gauge and sign displays can be treated as structural rather than ad hoc. Zero calibration is the fixed-point sanity check that the cost of the calibrated null input is null, so the ledger cannot smuggle a nonzero offset. Together with base-sans-two, sign-reversing, and monotone siblings, it closes the sans-anchor hypothesis bundle for this family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.