`Frequency`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 59.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  56abbrev Energy := ℝ
  57abbrev Action := ℝ
  58abbrev Mass := ℝ
  59abbrev Frequency := ℝ
  60abbrev Momentum := ℝ
  61abbrev Charge := ℝ
  62
  63/-! ## Canonical RS-native base units -/
  64
  65/-- One tick: the fundamental time quantum. -/
  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

papers checked against this theorem

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