rescale_potential

formal source

  49/-! ## Rescaling Operations -/
  50
  51/-- Rescale potential by factor α and offset b: p → αp + b -/
  52def rescale_potential (α b : ℝ) (p : ℝ) : ℝ := α * p + b
  53
  54/-- Rescale cost by factor k: J → kJ -/
  55def rescale_cost (k : ℝ) (J : ℝ) : ℝ := k * J
  56
  57/-! ## Gauge-Invariant Quantities -/
  58
  59/-- A quantity is gauge-invariant if rescaling doesn't change it. -/
  60def GaugeInvariant (f : ℝ → ℝ → ℝ → ℝ) : Prop :=
  61  ∀ (α k : ℝ) (hα : α ≠ 0) (hk : k ≠ 0) (x : ℝ),
  62    f α k x = f 1 1 x
  63
  64/-- Dimensionless ratios are gauge-invariant.
  65    If p₁/p₂ = r, then (αp₁ + b)/(αp₂ + b') = r when b = b' = 0. -/
  66theorem ratio_gauge_invariant (p₁ p₂ : ℝ) (hp₂ : p₂ ≠ 0) (α : ℝ) (hα : α ≠ 0) :
  67    (α * p₁) / (α * p₂) = p₁ / p₂ := by
  68  field_simp
  69  ring
  70
  71/-! ## Alpha is Dimensionless -/
  72
  73/-- α⁻¹ is a pure number (no units). -/
  74theorem alphaInv_dimensionless :
  75    ∃ (n : ℝ), Alpha.alphaInv = n ∧ n > 0 := by
  76  use Alpha.alphaInv
  77  constructor
  78  · rfl
  79  · -- Use the axiom that asserts the value
  80    rw [Alpha.alphaInv_predicted_value]
  81    norm_num
  82