`lambda_kin_eq_K_gate_ratio`

proved

show as: view math explainer →

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

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

formal source

 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))
 247
 248/-- Planck length in RS units: ℓ_P = c · τ_P. -/
 249noncomputable def planckLength_rs : Length :=
 250  c * planckTime_rs
 251
 252/-- Planck mass in RS units: m_P = √(ħc/G).
 253    This is the mass at which gravitational and quantum scales meet. -/
 254noncomputable def planckMass_rs : Mass :=
 255  Real.sqrt (hbarQuantum * c / Constants.G)
 256
 257/-- Planck energy in RS units: E_P = m_P · c² = m_P (since c = 1). -/

papers checked against this theorem

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