G_rs_eq

formal source

 146noncomputable def G_rs : ℝ := φ_val^(5 : ℤ)
 147
 148/-- G = φ^5 in RS-native units. -/
 149theorem G_rs_eq : G_rs = φ_val^5 := rfl
 150
 151/-- G > 0. -/
 152theorem G_pos : G_rs > 0 := by
 153  unfold G_rs
 154  exact pow_pos phi_pos 5
 155
 156/-- G is algebraic in φ. -/
 157theorem G_algebraic_in_φ : ∃ n : ℤ, G_rs = φ_val^n := ⟨5, by simp [G_rs]⟩
 158
 159/-- G · ℏ = φ^5 · φ^(-5) = 1.
 160    This is the RS version of ℏG/c³ being dimensionless. -/
 161theorem G_ℏ_product : G_rs * ℏ_rs = 1 := by
 162  unfold G_rs ℏ_rs E_coh τ₀
 163  simp only [mul_one]
 164  -- φ^5 * φ^(-5) = 1
 165  rw [zpow_neg, mul_inv_cancel₀]
 166  exact pow_ne_zero 5 phi_pos.ne'
 167
 168/-! ## Fine Structure Constant: α -/
 169
 170/-- The geometric seed for α: 1/137.
 171    This comes from the holographic area count. -/
 172noncomputable def α_seed : ℝ := 1 / 137
 173
 174/-- The gap-45 correction factor.
 175    This accounts for the integration gap D²(D+2) = 45 at D = 3. -/
 176noncomputable def gap_correction : ℝ := 1 + 45 / (360 * 137)
 177
 178/-- **Fine structure constant** (approximate).
 179