GaugeInvariant
plain-language theorem explainer
GaugeInvariant defines the property that a function f of three real arguments stays fixed when its first two inputs are set to unity, for any nonzero rescaling factors. Researchers separating gauge choices from physical parameters in ledger-based models cite it to show that dimensionless outputs survive unit rescalings. The definition encodes the invariance directly as a universal quantification over α and k.
Claim. A function $f : ℝ → ℝ → ℝ → ℝ$ is gauge-invariant when $f(α, k, x) = f(1, 1, x)$ holds for every nonzero real $α, k$ and every real $x$.
background
The module treats the objection that rescaling symmetries p → αp + b and J → kJ introduce free parameters. Gauge freedom denotes physically irrelevant unit choices, while parameters are dimensionless constants that remain after cancellation. The supplied module doc states that dimensionless ratios such as α⁻¹ are unchanged across gauges, matching the standard example that α equals 1/137.036 in SI, Gaussian, or natural units.
proof idea
The definition is a direct universal quantification stating the equality under rescaling; no lemmas or tactics are applied.
why it matters
It supplies the formal criterion used to establish that outputs such as α⁻¹ = 4π·11 - ln φ - 103/(102π⁵) are independent of gauge, thereby closing the argument that ledger theorems contain tunable constants. The definition appears among siblings that apply the same invariance to specific quantities including alphaInv_gauge_invariant and log_phi_gauge_invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.