`tau_rec`

definition

show as: view math explainer →

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

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

depends on

used by

formal source

 209/-! ## K-gate derived displays in RS-native units -/
 210
 211/-- Recognition time display: τ_rec = (2π)/(8 ln φ) · τ₀. -/
 212@[simp] noncomputable def tau_rec : Time :=
 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. -/

papers checked against this theorem

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