def
definition
total_solid_angle
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.PlanckScaleMatching on GitHub at line 181.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
178def num_octants : ℕ := 8
179
180/-- The total solid angle of a sphere = 4π. -/
181noncomputable def total_solid_angle : ℝ := 4 * Real.pi
182
183/-- Verification: 8 × (π/2) = 4π. -/
184theorem octants_cover_sphere :
185 (num_octants : ℝ) * solid_angle_per_octant = total_solid_angle := by
186 simp [num_octants, solid_angle_per_octant, total_solid_angle]
187 ring
188
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