powerGeneratedNativeCost
plain-language theorem explainer
Defines the native cost of the power map q ↦ q^n on ratio orbits: J(q^n) off the unit, and the zero orbit at q = 1. Anyone classifying structural PRC native costs (odd vs even powers, sign reversal) cites this carrier. The body is a two-branch composition of the rational power with the orbit-level J-cost.
Claim. For $n \in \mathbb{N}$ and ratio orbit $q$, the power-generated native cost is the zero orbit if the rational display of $q$ equals $1$, and otherwise the rational $J$-cost $J(x)=\frac{x+x^{-1}}{2}-1$ evaluated on the ratio-orbit section of $q^n$.
background
In the Primitive Recognition Calculus ledger, costs are maps on RatioOrbit: integer-numerator / nonzero-denominator displays of rationals (K4.7), with verifier transport toRat recovering the classical rational by cross-multiplication.
The PRC rational $J$-cost on a ratio orbit is onRatioOrbit: $J(q)=((q+q^{-1})/2)-1$, the discrete avatar of the T5 cost $J(x)=\cosh(\log x)-1$. The section ratioOrbitOfRat lifts a classical rational back to a ratio orbit so powers can be computed in $\mathbb{Q}$ and re-embedded.
This module builds a structural ledger of candidate native costs without the two-point calibration. Power-generated costs are the main infinite family: every exponent is admitted here; parity later splits sign-reversing (odd) from non-sign-reversing (even) members.
proof idea
Pure definition, not a proof. Branch on whether q.toRat = 1. The unit case returns RatioOrbit.zero (matching $J(1)=0$). Otherwise form the classical power q.toRat ^ n, re-section via ratioOrbitOfRat, and apply onRatioOrbit to obtain the ratio-orbit $J$-cost of that power.
why it matters
This is the common generator for the gauge-orbit family of native costs. Downstream, oddPowerGeneratedNativeCost k is the $(2k+1)$-power case ($k=0$ recovers the canonical cost; $k\ge 1$ are distinct orbit points), and evenPowerGeneratedNativeCost k is the $(2k+2)$-power case (carrier analogue of the continuum countermodel costLambdaTwo).
Sibling lemmas record that every power satisfies the reciprocal and monotonicity native-cost hypotheses, while sign reversal holds exactly off the even exponents. The open classification GaugeOrbitIsSignOrOddPowerFamily asserts every anchor-free structural inhabitant is either the zero-exponent sign cost or some odd-power generated cost—so this definition is the raw material of that dichotomy.
Framework link: the underlying $J$ is the T5 unique cost from the forcing chain; the ledger tests which discrete power morphisms still obey the structural native-cost axioms on ratio orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.