ell0_pos

formal source

 413/-- The fundamental length unit ℓ₀ in RS-native units (voxel). -/
 414@[simp] noncomputable def ell0 : ℝ := 1
 415
 416lemma ell0_pos : 0 < ell0 := by
 417  simp [ell0]
 418
 419/-- Light-cone identity: ℓ₀ = c · τ₀ (in RS-native units). -/
 420lemma c_ell0_tau0 : c * tau0 = ell0 := by
 421  simp [c, tau0, ell0, tick]
 422
 423/-- Fundamental recognition wavelength λ_rec.
 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φ⁵.