def
definition
lambda_kin
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 216.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
213 Constants.RSUnits.tau_rec_display U
214
215/-- Kinematic wavelength display: λ_kin = (2π)/(8 ln φ) · ℓ₀. -/
216@[simp] noncomputable def lambda_kin : Length :=
217 Constants.RSUnits.lambda_kin_display U
218
219theorem tau_rec_eq_K_gate_ratio :
220 tau_rec = Constants.RSUnits.K_gate_ratio := by
221 unfold tau_rec
222 have hlog : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
223 simp [Constants.RSUnits.tau_rec_display, Constants.RSUnits.K_gate_ratio, U, tick]
224 field_simp [hlog]
225 ring
226
227theorem lambda_kin_eq_K_gate_ratio :
228 lambda_kin = Constants.RSUnits.K_gate_ratio := by
229 unfold lambda_kin
230 have hlog : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
231 simp [Constants.RSUnits.lambda_kin_display, Constants.RSUnits.K_gate_ratio, U, voxel]
232 field_simp [hlog]
233 ring
234
235/-! ## Planck-Scale Quantities (RS-derived)
236
237In RS, the Planck scale emerges from the gate identities, not as a postulate.
238These are expressed in RS-native units.
239-/
240
241/-- Planck time in RS units: τ_P = √(ħG/c⁵).
242 In RS-native units, this is a dimensionless φ-expression. -/
243noncomputable def planckTime_rs : Time :=
244 -- Using the gate identity: τ_P = τ₀ · √(G/c³) where G,c are in RS units
245 -- Since c = 1, and G is derived, this is pure φ-structure
246 tick * Real.sqrt (Constants.G / (c ^ 3))