jcost_rpow_inv
plain-language theorem explainer
Recognition cost is invariant under inverting the base before a real power: J(x^l) equals J((x^{-1})^l) for x>0. Continuum gauge arguments cite this to reduce to bases above one. The proof rewrites the inverted power as an inverse, then applies J-symmetry.
Claim. For every real $x>0$ and every real exponent $\ell$, if $J(t)=\frac{t+t^{-1}}{2}-1$ denotes recognition cost on positive reals, then $J(x^{\ell})=J((x^{-1})^{\ell})$.
background
Recognition cost on a positive ratio is the T5 J-functional $J(t)=(t+t^{-1})/2-1$. It is the unique continuous cost compatible with the Recognition Composition Law once normalization and convexity are fixed. A basic identity is symmetry under inversion: $J(t)=J(t^{-1})$ for $t>0$.
This module studies how a preferred unit scale is selected by least cost on discrete gauges, and why that selection fails on the continuum. Real powers $x^\ell$ appear as continuous gauge rescalings of a fixed base ratio $x$. The doc-comment states the local purpose: cost is blind to base inversion, so gauge claims need only be proved for bases above one; real exponents are required for the continuum half of the argument.
proof idea
First record positivity of $x^\ell$ from $x>0$ via Real.rpow_pos_of_pos. Rewrite $(x^{-1})^\ell$ as $(x^\ell)^{-1}$ by Real.inv_rpow. The goal becomes $J(x^\ell)=J((x^\ell)^{-1})$, which is exactly Jcost_symm on the positive quantity $x^\ell$. Three-line tactic proof; no new cost identities.
why it matters
Parent use is no_least_gauge_member: on the continuum, every admissible scale has a strictly cheaper half-scale, so least-cost cannot pick a unit the way it does on a countable carrier. That theorem reduces the $x<1$ case by inverting the base and transporting inequalities through this identity (rewriting both $J(x^{\ell/2})$ and $J(x^\ell)$).
In the forcing chain this sits under T5 J-uniqueness: once $J$ is fixed, gauge statements about powers inherit inversion blindness for free. It is bookkeeping for continuum versus discrete unit selection, not a new physical constant, but without it the continuum non-existence argument would double in cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.