powerGeneratedNativeCost_toRat
plain-language theorem explainer
The rational display of the native cost generated by the power map q ↦ q^n equals the classical J-cost of the n-th power of q's rational. Anyone verifying that power maps induce PRC native-cost structure cites this transport identity. The proof unfolds the definition and case-splits on whether the orbit is the unit ratio.
Claim. For every natural number $n$ and every ratio orbit $q$, the rational display of the native cost generated by $q \mapsto q^n$ equals $J(r^n)$, where $r$ is the rational display of $q$ and $J(t)=(t+t^{-1})/2-1$.
background
In the primitive recognition calculus, a ratio orbit packages an integer numerator over a nonzero distinction-nat denominator. Its verifier display toRat is the ordinary rational $num/den$. The structural ledger works with these orbits rather than bare rationals, then transports statements back via toRat.
The J-display on rationals is $J(t)=(t+t^{-1})/2-1$, the same cost forced by T5 uniqueness in the forcing chain. The power-generated native cost at exponent $n$ is defined by cases: if the orbit displays as $1$, return the zero orbit; otherwise wrap $J$ around the orbit of $r^n$. The companion lemma jq_onRatioOrbit already identifies the on-orbit cost with $J$ of the rational display.
This module builds a structural ledger of candidate native costs and checks which generators satisfy the PRC hypotheses (reciprocal symmetry, monotonicity, sign reversal, zero calibration).
proof idea
Term-mode case split after unfolding the definition of the power-generated cost. If the orbit displays as $1$, the definition returns the zero orbit; zero_toRat, $1^n=1$, and a norm_num evaluation of $J(1)$ close the equality. If not, rewrite with the negative branch, apply jq_onRatioOrbit (which equates the on-orbit cost's rational to $J$ of the display), and finish with ratioOrbitOfRat_toRat recovering the powered rational.
why it matters
This is the transport lemma that lets every subsequent property of power-generated costs be checked on ordinary rationals via $J$. Downstream it discharges the reciprocal clause in powerGeneratedNativeCost_base, feeds monotonicity (powerGeneratedNativeCost_monotone), zero calibration, and both the positive and negative sign-reversal theorems that separate odd from even exponents. The odd-power specialization is a one-line application of this identity.
In the Recognition framework the identity ties the ledger back to T5 J-uniqueness: the only cost compatible with the Recognition Composition Law is $J(x)=(x+x^{-1})/2-1$. Parity of the exponent then decides orientation reversal, which is exactly the membership cut used to isolate the canonical odd-power generators. Without this bridge, the structural ledger could not certify that power maps realize native costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.