`tick`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 66.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  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

papers checked against this theorem

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