`ExternalCalibration`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 292.

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

The Speed of Light · foundational / THEOREM
c is one voxel per tick by construction; the SI value 299,792,458 m/s is a unit conversion, not a measurement of the universe

depends on

used by

formal source

 289-/
 290
 291/-- External calibration structure for mapping RS units to SI/other systems. -/
 292structure ExternalCalibration where
 293  /-- Seconds per tick (τ₀ in seconds). -/
 294  seconds_per_tick : ℝ
 295  /-- Meters per voxel (ℓ₀ in meters). -/
 296  meters_per_voxel : ℝ
 297  /-- Joules per coherence quantum. -/
 298  joules_per_coh : ℝ
 299  /-- All conversion factors are positive. -/
 300  seconds_pos : 0 < seconds_per_tick
 301  meters_pos : 0 < meters_per_voxel
 302  joules_pos : 0 < joules_per_coh
 303  /-- Consistency: c = ℓ₀/τ₀ must equal 299792458 m/s in SI. -/
 304  speed_consistent : meters_per_voxel / seconds_per_tick = 299792458
 305
 306/-- Convert time (in ticks) to seconds. -/
 307@[simp] noncomputable def to_seconds (cal : ExternalCalibration) (t : Time) : ℝ :=
 308  t * cal.seconds_per_tick
 309
 310/-- Convert length (in voxels) to meters. -/
 311@[simp] noncomputable def to_meters (cal : ExternalCalibration) (L : Length) : ℝ :=
 312  L * cal.meters_per_voxel
 313
 314/-- Convert velocity (in voxels/tick) to m/s. -/
 315@[simp] noncomputable def to_m_per_s (cal : ExternalCalibration) (v : Velocity) : ℝ :=
 316  v * (cal.meters_per_voxel / cal.seconds_per_tick)
 317
 318/-- Convert energy (in coh) to Joules. -/
 319@[simp] noncomputable def to_joules (cal : ExternalCalibration) (E : Energy) : ℝ :=
 320  E * cal.joules_per_coh
 321
 322/-- Convert mass (in coh/c²) to kg. -/

papers checked against this theorem

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