`ell_P`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.PlanckScaleMatching
domain: Constants
line: 192 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.PlanckScaleMatching on GitHub at line 192.

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

 189/-! ## Part 5: The Planck-Scale Relationship -/
 190
 191/-- The Planck length ℓ_P = √(ℏG/c³). -/
 192noncomputable def ell_P : ℝ := sqrt (hbar * G / c^3)
 193
 194/-- The Planck length is positive. -/
 195theorem ell_P_pos : ell_P > 0 := by
 196  unfold ell_P
 197  apply sqrt_pos.mpr
 198  apply div_pos
 199  · exact mul_pos hbar_pos G_pos
 200  · exact pow_pos c_pos 3
 201
 202/-- **THE PLANCK GATE IDENTITY**:
 203
 204λ_rec = √(ℏG/(πc³)) = ℓ_P / √π
 205
 206This follows from the face-averaging principle applied to the
 207curvature extremum. -/
 208noncomputable def lambda_rec_SI : ℝ := sqrt (hbar * G / (Real.pi * c^3))
 209
 210/-- λ_rec_SI > 0. -/
 211theorem lambda_rec_SI_pos : lambda_rec_SI > 0 := by
 212  unfold lambda_rec_SI
 213  apply sqrt_pos.mpr
 214  apply div_pos
 215  · exact mul_pos hbar_pos G_pos
 216  · exact mul_pos Real.pi_pos (pow_pos c_pos 3)
 217
 218/-- **THE 0.564 FACTOR**:
 219
 220λ_rec/ℓ_P = 1/√π ≈ 0.564.
 221
 222This is the key result of Conjecture C8. -/

papers checked against this theorem

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