def
definition
K_rs
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 269.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
266noncomputable def alphaInv_rs : ℝ := Constants.alphaInv
267
268/-- The K-gate ratio: K = π/(4 ln φ). -/
269noncomputable def K_rs : ℝ := Constants.RSUnits.K_gate_ratio
270
271/-- Coherence scaling: E_coh = φ⁻⁵. -/
272noncomputable def E_coh_rs : ℝ := phiRung (-5)
273
274lemma E_coh_rs_eq_E_coh : E_coh_rs = E_coh := by
275 simp only [E_coh_rs, phiRung, E_coh, cLagLock]
276 -- Both are phi^(-5), but one uses zpow and the other uses rpow
277 -- φ^(-5 : ℤ) = φ^(-5 : ℝ) for φ > 0
278 have h : phi ^ (-5 : ℤ) = phi ^ ((-5 : ℤ) : ℝ) := by
279 rw [← Real.rpow_intCast phi (-5)]
280 rw [h]
281 congr 1
282 norm_cast
283
284/-! ## External Calibration (SI Bridge)
285
286If you want "seconds" and "meters", you must provide an explicit calibration
287mapping RS primitives to an external unit system. This keeps the empirical
288seam explicit and auditable.
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. -/