rescale_cost
plain-language theorem explainer
rescale_cost implements the J-rescaling map J → kJ as a direct multiplication on the reals. Gauge-invariance arguments in Recognition Science cite it when demonstrating that dimensionless outputs such as α^{-1} remain unchanged under unit choices. The definition is a one-line algebraic assignment with no lemmas or reductions.
Claim. The rescaled cost is defined by $kJ$, where $k$ is any real rescaling factor and $J$ is the original cost.
background
Module Bridge.GaugeVsParams resolves the objection that ledger rescalings p → αp + b and J → kJ introduce free parameters. It distinguishes gauge freedom (physically irrelevant unit choices) from tunable dimensionless constants. The supplied DOC_COMMENT states the map explicitly as J → kJ. Upstream results supply supporting primitives such as active edge count A from IntegrationGap and coherence energy units from Masses.Anchor, but the present definition uses only real multiplication.
proof idea
One-line definition that applies ordinary multiplication on ℝ.
why it matters
The definition supplies the explicit rescaling operation needed to prove gauge invariance of dimensionless quantities such as α^{-1} = 4π·11 - ln φ - 103/(102π⁵). It directly supports the module's resolution that gauge factors cancel in observables, consistent with the Recognition Science treatment of units. No downstream theorems are recorded, so the definition functions as a shared primitive for later invariance statements in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.