def
definition
solid_angle_per_octant
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.PlanckScaleMatching on GitHub at line 175.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
172/-! ## Part 4: Face-Averaging and the π Factor -/
173
174/-- The solid angle per octant = π/2 steradians. -/
175noncomputable def solid_angle_per_octant : ℝ := Real.pi / 2
176
177/-- There are 8 octants in 3D space. -/
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