lambda_rec_SI

formal source

 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
 226  have hpic3_pos : Real.pi * c^3 > 0 := mul_pos Real.pi_pos (pow_pos c_pos 3)
 227  have hc3_pos : c^3 > 0 := pow_pos c_pos 3
 228  have hhG_pos : hbar * G > 0 := mul_pos hbar_pos G_pos
 229  have hhG_nonneg : hbar * G ≥ 0 := le_of_lt hhG_pos
 230  have hpi_nonneg : (0 : ℝ) ≤ Real.pi := le_of_lt Real.pi_pos
 231  rw [sqrt_div hhG_nonneg, sqrt_div hhG_nonneg]
 232  have h_c3_eq : sqrt (Real.pi * c^3) = sqrt Real.pi * sqrt (c^3) :=
 233    sqrt_mul hpi_nonneg (c^3)
 234  rw [h_c3_eq]
 235  have h_sqrt_c3_ne : sqrt (c^3) ≠ 0 := (sqrt_pos.mpr hc3_pos).ne'
 236  have h_sqrt_pi_ne : sqrt Real.pi ≠ 0 := (sqrt_pos.mpr Real.pi_pos).ne'
 237  have h_sqrt_hG_ne : sqrt (hbar * G) ≠ 0 := (sqrt_pos.mpr hhG_pos).ne'
 238  field_simp [h_sqrt_c3_ne, h_sqrt_pi_ne, h_sqrt_hG_ne]