costLambda_gauge_transitive
plain-language theorem explainer
Any two positive-parameter members of the native cost family are related by a multiplicative automorphism of the positive reals: F_λ(x) equals F_μ at x raised to λ/μ. Citation target for the calibration-as-gauge claim and for four-law completeness. Proof is a short unfold-and-rewrite using real power multiplication identities.
Claim. For all real $l,m,x$ with $m>0$ and $x>0$, the $\lambda$-parameterized cost satisfies $F_l(x)=F_m\bigl(x^{l/m}\bigr)$. Equivalently, the multiplicative automorphism $x\mapsto x^{l/m}$ of $(\mathbb{R}_{>0},\times)$ carries the family member at parameter $m$ onto the member at parameter $l$.
background
In the Primitive Recognition Calculus, admissible costs on the positive reals form a one-parameter family $F_\lambda$, written costLambda in the development. Each member is the classical J-cost post-composed with a power map: $F_\lambda = J\circ(\cdot^\lambda)$, where $J(x)=(x+x^{-1})/2-1$ is the unique reciprocal cost fixed by the Recognition Composition Law once curvature at the unit is normalized.
The Calibration axiom (second log-coordinate derivative at the origin equals 1) singles out $\lambda=1$ and recovers $J$. Without that external unit choice, the composition law alone is invariant along the whole positive-parameter family. The present statement upgrades the pointwise representation "each member is $J$ after a power" to a homogeneous orbit statement: any member reaches any other by an automorphism of $(\mathbb{R}_{>0},\times)$.
Local setting is native-cost uniqueness inside PRC: the four algebraic laws plus positive log-curvature characterize exactly this gauge orbit.
proof idea
Short tactic proof. From $m>0$ obtain $(l/m)\cdot m=l$ and $(l/m)\cdot(-m)=-l$. Unfold the definition of the parameterized cost (which applies real powers $x^{\pm\lambda}$ inside $J$). Rewrite both sides with Real.rpow_mul (using $x\ge 0$) and cancel via the two scalar identities. No analytic lemmas beyond power arithmetic are required.
why it matters
This is the exact transitivity half of the gauge-torsor picture for native costs. Downstream, costLambda_injective proves freeness (distinct positive exponents give distinct functions, via log-curvature $\lambda^2$ at the unit), and the doc-comment on that result explicitly pairs the two: action free and transitive, so ${F_\lambda:\lambda>0}$ is a principal homogeneous space under the gauge group.
The same lemma is used by prc_four_law_completeness (T1′ closed): every positive-curvature solution of the four laws equals some $F_c$ with $c>0$, so the solution set is exactly the gauge orbit. Calibration $\lambda=1$ is then the only residual freedom that isolates $J$, matching the T5 J-uniqueness landmark and the CostAxioms Calibration class (second derivative at zero equals 1). Without transitivity one could not assert that the algebra distinguishes no preferred basepoint inside the family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.