powerGeneratedNativeCost_base
plain-language theorem explainer
For every natural n, the native cost obtained by feeding the n-th power of a ratio orbit into the J-cost satisfies reciprocal symmetry, normalization invariance, the Recognition Composition Law, and unit-zero, i.e. the full PRC native-cost package minus two-point calibration. Even- and odd-power structural certificates cite it as their base field. Each structure field is discharged by transporting through toRat and invoking the matching jq identity.
Claim. For every $n \in \mathbb{N}$, the cost $q \mapsto J(q^n)$ on ratio orbits satisfies reciprocal symmetry $C(q^{-1})=C(q)$, normalization invariance, the Recognition Composition Law $C(xy)+C(x/y)=2C(x)C(y)+2C(x)+2C(y)$, and $C(1)=0$, i.e. the native-cost hypothesis package excluding two-point calibration.
background
In the Primitive Recognition Calculus structural ledger, native costs are functionals on ratio orbits (integer-rational equivalence classes of positive ratios, with a verifier display toRat). The base cost character is jq, the discrete J-cost $J(x)=(x+x^{-1})/2-1$ evaluated on that display; siblings record that jq is nonnegative, vanishes only at the unit orbit, and obeys the Recognition Composition Law (RCL).
powerGeneratedNativeCost n is the cost obtained by composing jq with the n-th power map on ratio orbits: on the rational display it is $q \mapsto J(q^n)$. The target structure PRCNativeCostHypothesesSansTwoCalibration packages four axioms: reciprocal symmetry under orbit inversion, invariance under ratio normalization, the canonical RCL identity, and vanishing at the unit orbit. Two-point calibration is deliberately omitted.
Upstream transport lemmas (crossEq_iff_toRat_eq, add_toRat, mul_toRat, recip_toRat, one_toRat) identify cross-multiplication equality of orbits with ordinary rational equality, so every ledger identity can be checked after pushing to \mathbb{Q}.
proof idea
Structure-field tactic proof with four independent discharges, each reducing through toRat.
reciprocal: rewrite bycrossEq_iff_toRat_eqand the twopowerGeneratedNativeCost_toRatinstances; applyrecip_toRat,inv_pow, andjq_inv.normalized_invariant: same crossEq/toRat bridge, thenDistinctionNat.normalizeRatio_toRat.canonical_rcl: expand addition and multiplication of orbits viaadd_toRat/mul_toRat/div_toRat/two_toRat, push powers withmul_pow/div_pow, and finish byjq_rclon the nonzero powered displays (pow_ne_zero).unit_zero: unfold the definition and hit theif_posbranch withone_toRat.
No new algebraic content beyond the jq identities and power laws.
why it matters
This is the uniform base certificate that every pure power of the J-cost still obeys the structural native-cost axioms (sans two-calibration). Downstream, evenPowerGeneratedNativeCost_sans_signReversing invokes it at even exponents $2k+2$ to isolate sign-reversal as the single missing field, and oddPowerGeneratedNativeCost_sansAnchor invokes it at odd exponents $2k+1$ inside the anchor-free structural package.
In the Recognition forcing chain the RCL and J-uniqueness (T5) force the cost shape; power-generated costs probe which discrete symmetries survive under the phi-ladder and eight-tick octave. The theorem shows the ledger axioms are stable under powering, so later uniqueness or calibration arguments can treat the whole power family at once rather than re-proving RCL for each exponent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.