theorem
proved
term proof
alphaInv_gauge_invariant
show as:
view Lean formalization →
formal statement (Lean)
114theorem alphaInv_gauge_invariant :
115 ∀ (α k b : ℝ) (hα : α ≠ 0) (hk : k ≠ 0),
116 Alpha.alphaInv = Alpha.alphaInv := by
proof body
Term-mode proof.
117 intro _ _ _ _ _
118 rfl
119
120/-! ## The Physical Argument -/
121
122/-- Gauge vs Parameter distinction:
123
124 **Gauge**: A choice that doesn't affect physical predictions.
125 - Example: Choosing meters vs feet doesn't change physics.
126 - Test: Do dimensionless outputs change? NO → Gauge.
127
128 **Parameter**: A tunable constant that changes predictions.
129 - Example: Changing α in QED changes cross-sections.
130 - Test: Do dimensionless outputs change? YES → Parameter.
131
132 **RS Rescalings**:
133 - p → αp + b: Doesn't change α⁻¹ → Gauge
134 - J → kJ: Doesn't change α⁻¹ → Gauge
135
136 Therefore: RS has zero parameters, only gauge choices. -/