`Action`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.RSNativeUnits
domain: Constants
line: 57 · 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 57.

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

used by

formal source

  54abbrev Length := ℝ
  55abbrev Velocity := ℝ
  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

papers checked against this theorem

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