rescale_potential
rescale_potential defines the affine map that sends potential p to αp + b. Gauge-invariance arguments in the ledger formalism cite it to separate unit choices from physical parameters. The definition is a direct algebraic expression with no lemmas or reductions.
claimThe affine rescaling map on the potential given by $pmapsto alphap + b$ for real scalars $alpha$ and $b$.
background
The module distinguishes gauge freedom (continuous rescalings of units) from tunable dimensionless parameters. It shows that quantities such as $alpha^{-1}$ remain unchanged once all gauge factors cancel. Upstream, cost is the J-cost of a recognition event or the derived cost induced by a multiplicative recognizer comparator.
proof idea
One-line definition that directly encodes the stated affine transformation.
why it matters in Recognition Science
It supplies the concrete map used to prove that dimensionless outputs such as $alpha^{-1}$ are gauge-invariant, closing the objection that ledger rescalings introduce free parameters. The construction supports the siblings that establish invariance of $alphaInv$, $logphi$, and curvature under the same transformation.
scope and limits
- Does not assert invariance of any concrete observable.
- Does not fix numerical values for the gauge parameters alpha or b.
- Does not relate the potential rescaling to the separate cost rescaling J to kJ.
formal statement (Lean)
52def rescale_potential (α b : ℝ) (p : ℝ) : ℝ := α * p + b
proof body
Definition body.
53
54/-- Rescale cost by factor k: J → kJ -/