gauge_action_transitive
plain-language theorem explainer
The positive-real gauge action on the one-parameter cost family F_c(t)=cosh(c t)-1 is transitive: any two members with positive scales are related by a positive rescaling of the log-coordinate. Cited by anyone showing residual cost freedom is a single real torsor under (R>0,·). Proof is a direct witness μ=d/c plus field simplification.
Claim. For all positive real scales $c,d>0$, there exists $\mu>0$ such that the functions $t\mapsto\cosh(c(\mu t))-1$ and $t\mapsto\cosh(d\,t)-1$ are identical on $\mathbb{R}$.
background
In the Primitive Recognition Calculus calibration target, continuous costs form a one-parameter family $F_c(t)=\cosh(c t)-1$ for $c>0$. This is the continuous avatar of the J-cost $J(x)=\cosh(\log x)-1$ after a linear change of the log-coordinate (T5 forces that shape). The gauge action of the positive reals is $\mu\bullet F:=F(\mu,\cdot)$, i.e. positive rescaling of the argument.
The local goal is Item 2 sharpened: after the discrete $\delta$ structure is fixed, residual continuous freedom in the cost should be exactly one real (a unit of scale). Freeness of the same action is the sibling injectivity statement on log-curvature; transitivity is the complementary half needed for a torsor.
proof idea
Construct the witness $\mu=d/c$. Positivity is immediate from $d,c>0$ via division of positives. Functional extensionality reduces equality of the two cosh expressions to a pointwise identity. The algebraic key $c\cdot((d/c)\cdot t)=d\cdot t$ is discharged by field simplification, using $c\neq 0$ from $c>0$. Rewrite and done. No external lemmas beyond basic real arithmetic.
why it matters
This is the transitive half of the free-and-transitive package that exhibits the cost family as a principal homogeneous space under $(\mathbb{R}_{>0},\cdot)$. The parent theorem cost_freedom_is_one_real_torsor conjoins freeness (log-curvature injectivity) with this result and concludes residual freedom is exactly one positive real, the unit of scale. That unit is fixed by one calibration datum (curvature 1), which the discrete $\delta$ structure does not supply.
In the Recognition framework this pins the continuous leftover after T5 J-uniqueness forces $J(x)=\cosh(\log x)-1$: the functional equation fixes the shape, and only overall scale remains for calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.