octants_cover_sphere
plain-language theorem explainer
The identity that eight octants each subtending π/2 steradians cover the full 4π solid angle of a sphere is verified. Workers deriving the recognition wavelength λ_rec from curvature extremum in the PlanckScaleMatching module cite this step when restoring the factor of 1/π from face averaging. The proof reduces immediately by substitution of the constant definitions followed by algebraic normalization.
Claim. In three-dimensional Euclidean space, $8$ times the solid angle per octant equals the total solid angle of the sphere: $8$ × (π/2) = 4π.
background
The PlanckScaleMatching module derives λ_rec ≈ 0.564 ℓ_P from the ledger-curvature extremum. It begins with the bit cost J_bit = J(φ) obtained from the unique cost functional, equates it to the curvature cost J_curv(λ) = 2λ² distributed over the eight faces of the Q₃ hypercube, and solves for the recognition wavelength. Restoring SI units via c³λ²/(ℏG) and averaging over the eight-face geometry introduces the factor 1/π, yielding λ_rec = √(ℏG/(π c³)) = ℓ_P/√π. The upstream definitions supply the geometric constants: num_octants := 8, solid_angle_per_octant := π/2, and total_solid_angle := 4π.
proof idea
The proof is a one-line wrapper that applies simp to unfold the three constant definitions, then invokes the ring tactic to confirm the numerical identity 8 × (π/2) = 4π.
why it matters
This identity closes the geometric averaging step in the derivation of λ_rec = ℓ_P/√π from the ledger-curvature argument of Conjecture C8. It supplies the explicit factor 1/π that appears in the RS-native expression for G = λ_rec² c³ / (π ℏ). The step sits between the J_curv definition and the final Planck ratio in the module chain; downstream uses of G inherit the averaging directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.