cost_laws_gauge_invariant
plain-language theorem explainer
Any positive power reparametrization $x\mapsto x^a$ preserves the four algebraic cost laws: reciprocal symmetry, normalization at 1, the Recognition Composition Law, and continuity on the positives. Citation target for anyone closing four-law completeness of the native cost. The proof is a direct four-conjunct refinement that pushes the power through each identity via real rpow lemmas.
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ and $a>0$. Suppose $F$ is reciprocal ($F(x)=F(x^{-1})$ for all $x>0$), normalized ($F(1)=0$), satisfies the composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for $x,y>0$, and is continuous on $(0,\infty)$. Then the gauged map $x\mapsto F(x^a)$ obeys the same four properties.
background
In the Primitive Recognition Calculus cost track, admissible costs on the positive reals are cut out by four laws: reciprocal symmetry $F(x)=F(x^{-1})$, normalization $F(1)=0$, the Recognition Composition Law (RCL) $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, and continuity on $(0,\infty)$. The shifted form $H=F+1$ converts RCL into d'Alembert's equation, the route used upstream to force the cosh-type solutions (and thence $J(x)=(x+x^{-1})/2-1$ after calibration).
The multiplicative group $\mathrm{Aut}(\mathbb{R}_{>0},\times)$ acts by gauge substitutions $x\mapsto x^a$ for $a>0$. The costLambda family is exactly the orbit of the calibrated $J$-cost under this action. Prior stratification already shows the family sits inside the four-law solution set and that non-$J$ gauges exist; what was missing is that the action maps every four-law solution to another four-law solution.
This module isolates that structural fact before the remaining analytic blocker (PRCFourLawCompletenessTarget): every non-trivial solution is gauge-equivalent to a unit-curvature calibrated one.
proof idea
Term-mode refine into the four conjuncts.
Reciprocal: for $x>0$, positivity of $x^a$ plus Real.inv_rpow reduces $F(x^a)=F((x^{-1})^a)$ to the reciprocal hypothesis at $x^a$.
Normalization: Real.one_rpow gives $1^a=1$, so $F(1^a)=F(1)=0$.
Composition: Real.mul_rpow and Real.div_rpow rewrite $(xy)^a$ and $(x/y)^a$ as products and quotients of powers; the composition hypothesis at the positive points $x^a,y^a$ finishes it.
Continuity: $x\mapsto x^a$ is continuous on $(0,\infty)$ for $a>0$ and maps the open positives into themselves; compose with the assumed continuity of $F$ on that set.
No functional-equation classification is invoked; only elementary real-power identities.
why it matters
This is the structural half of four-law completeness for native costs. Downstream, cost_laws_complete_of_calibratable consumes it together with the isolated calibratability hypothesis PRCFourLawCompletenessTarget and the law-of-logic forcing of calibrated $J$, to conclude that every non-trivial four-law solution with positive log-curvature lies in the costLambda family. Combined with the already-proved inclusion family ⊆ solutions, that yields the biconditional: residual freedom is exactly the positive gauge orbit.
In framework terms this stabilizes the solution set as a union of $\mathrm{Aut}(\mathbb{R}_{>0},\times)$-orbits, so the only remaining distinction among members is the curvature-normalization step that pins the calibrated representative to $J$ (T5 J-uniqueness, RCL). The honest open piece is still the free-frequency d'Alembert classification (continuous solutions $\cosh(c\cdot)$ with positivity killing the oscillatory branch), deliberately left as PRCFourLawCompletenessTarget rather than asserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.