lambda_rec_pos

formal source

 424    In the 8-tick cycle, λ_rec = ℓ₀ (in RS-native units). -/
 425noncomputable def lambda_rec : ℝ := ell0
 426
 427lemma lambda_rec_pos : 0 < lambda_rec := by
 428  simp [lambda_rec]
 429
 430/-- Newton's gravitational constant G derived from first principles (RS-native form).
 431    \(G = \lambda_{\text{rec}}^2 c^3 / (\pi \hbar)\). -/
 432noncomputable def G : ℝ := (lambda_rec^2) * (c^3) / (Real.pi * hbar)
 433
 434lemma G_pos : 0 < G := by
 435  unfold G
 436  apply div_pos
 437  · apply mul_pos
 438    · exact pow_pos lambda_rec_pos 2
 439    · exact pow_pos c_pos 3
 440  · apply mul_pos
 441    · exact Real.pi_pos
 442    · exact hbar_pos
 443
 444/-- Einstein coupling constant κ = 8πG/c⁴ in RS-native units.
 445    Using G = λ_rec² c³ / (π ℏ) with λ_rec = c = 1 and ℏ = φ⁻⁵:
 446    κ = 8π · (φ⁵/π) / 1 = 8φ⁵.
 447
 448    This is the coefficient in front of T_μν in the Einstein field equations. -/
 449noncomputable def kappa_einstein : ℝ := 8 * Real.pi * G / (c^4)
 450
 451lemma kappa_einstein_eq : kappa_einstein = 8 * phi ^ (5 : ℝ) := by
 452  unfold kappa_einstein G hbar cLagLock lambda_rec ell0 c tau0 tick
 453  simp only [one_pow, mul_one, div_one]
 454  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 455  field_simp [hpi]
 456  rw [Real.rpow_neg phi_pos.le]
 457  field_simp [phi_ne_zero]