rescale_potential
plain-language theorem explainer
rescale_potential supplies the affine map sending potential p to αp + b. Gauge-invariance arguments in Recognition Science cite this map when separating coordinate choices from physical constants. The definition consists of the explicit linear expression with no supporting lemmas.
Claim. The rescaling map on potential is the function $pmapsto alphap + b$ for real parameters $alpha, b$.
background
The module examines the objection that ledger rescaling symmetries imply free parameters in the theory. It distinguishes gauge freedom (unit choices, physically irrelevant) from tunable parameters (physically meaningful), with the key point that dimensionless quantities such as $alpha^{-1}$ remain invariant because gauge factors cancel. Upstream results define cost as the derivedCost of a multiplicative recognizer's comparator and, separately, as the J-cost of a recognition event.
proof idea
The declaration is the direct definition of the affine transformation on the potential.
why it matters
This definition supports the argument that gauge transformations do not introduce tunable parameters, as they cancel in dimensionless observables such as the inverse fine-structure constant. It contributes to closing Gap 3 by formalizing the rescaling operation referenced in the module's resolution of the gauge objection. The module notes that $alpha^{-1}$ equals $4pi cdot 11 - ln phi - 103/(102pi^5)$ in all gauges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.