`ell_P_pos`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.PlanckScaleMatching on GitHub at line 195.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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. -/
 223theorem lambda_rec_over_ell_P :
 224    lambda_rec_SI / ell_P = 1 / sqrt Real.pi := by
 225  unfold lambda_rec_SI ell_P

papers checked against this theorem

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