pith. machine review for the scientific record. sign in
def

U

definition
show as:
view math explainer →
module
IndisputableMonolith.Constants.RSNativeUnits
domain
Constants
line
79 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

Derivations using this theorem

depends on

used by

formal source

  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
 100/-- Convert energy count (in coh) to raw RS scale. -/
 101@[simp] noncomputable def energy_raw (E : Energy) : ℝ := E * cohQuantum
 102
 103/-- Action quantum: ħ = E_coh · τ₀ = E_coh in RS-native units. -/
 104@[simp] noncomputable def hbarQuantum : ℝ := cohQuantum * tick
 105
 106/-- Convert action count (in act) to raw RS scale. -/
 107@[simp] noncomputable def action_raw (A : Action) : ℝ := A * hbarQuantum
 108
 109@[simp] lemma hbarQuantum_eq_Ecoh : hbarQuantum = E_coh := by

papers checked against this theorem

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