pith. machine review for the scientific record. sign in
theorem proved term proof

alphaInv_dimensionless

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  74theorem alphaInv_dimensionless :
  75    ∃ (n : ℝ), Alpha.alphaInv = n ∧ n > 0 := by

proof body

Term-mode proof.

  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
  83/-! ## Main Theorem: Alpha is Gauge-Invariant -/
  84
  85/-- The components of α⁻¹ do not depend on potential rescaling.
  86
  87    - 4π·11: Pure geometry (edge count × solid angle)
  88    - ln φ: Dimensionless (ratio of scales)
  89    - 103/(102π⁵): Pure number (topology × geometry)
  90
  91    None of these depend on the choice of p-scale or J-scale. -/

depends on (14)

Lean names referenced from this declaration's body.