def
definition
c
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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