def
definition
c
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants on GitHub at line 408.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
405 exact ⟨hbar_lower, hbar_upper⟩
406
407/-- The speed of light c in RS-native units (voxel/tick). -/
408@[simp] noncomputable def c : ℝ := 1
409
410lemma c_pos : 0 < c := by
411 simp [c]
412
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