`voxel`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.RSNativeUnits
domain: Constants
line: 69 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  66@[simp] def tick : Time := Constants.tick
  67
  68/-- One voxel: the fundamental length quantum. -/
  69@[simp] def voxel : Length := 1
  70
  71/-! ## Derived speed of light in RS-native units -/
  72
  73/-- Speed of light: c = ℓ₀/τ₀ = 1 voxel/tick. -/
  74@[simp] def c : Velocity := 1
  75
  76/-! ## Canonical `RSUnits` pack for bridge/cert code -/
  77
  78/-- RS-native gauge: τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1. -/
  79@[simp] noncomputable def U : RSUnits :=
  80{ tau0 := tick
  81, ell0 := voxel
  82, c := c
  83, c_ell0_tau0 := by simp [tick, voxel, c] }
  84
  85@[simp] lemma U_tau0 : U.tau0 = 1 := rfl
  86@[simp] lemma U_ell0 : U.ell0 = 1 := rfl
  87@[simp] lemma U_c : U.c = 1 := rfl
  88
  89/-! ## Coherence and action quanta
  90
  91`Constants.E_coh = φ⁻⁵` is a **dimensionless** RS-derived number.
  92In the RS-native system:
  93- **1 coh** (energy quantum) := E_coh
  94- **1 act** (action quantum) := ħ = E_coh · τ₀ = E_coh (since τ₀ = 1)
  95-/
  96
  97/-- Coherence energy quantum: φ⁻⁵ ≈ 0.0902. -/
  98@[simp] noncomputable def cohQuantum : ℝ := E_coh
  99

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.