total_solid_angle
plain-language theorem explainer
The declaration defines the total solid angle of a sphere as 4π in the reals. It is referenced by the octants_cover_sphere theorem inside the ledger-curvature derivation of the recognition wavelength. The definition is a direct noncomputable assignment that supplies the geometric factor needed for the 1/π restoration in the Planck ratio.
Claim. The total solid angle subtended by a sphere equals $4π$.
background
The PlanckScaleMatching module derives λ_rec ≈ 0.564 ℓ_P by equating bit cost J_bit = J(φ) to curvature cost J_curv(λ) = 2λ² and restoring SI dimensions via face averaging over the Q₃ hypercube. This averaging step introduces the factor 1/π, which is supplied by the total solid angle. The module imports PhiForcing to access J(x) = ½(x + x⁻¹) - 1 and Cost to connect the self-similar fixed point φ to the eight-face geometry.
proof idea
The definition is a direct assignment total_solid_angle := 4 * Real.pi. It functions as a one-line wrapper that supplies the standard solid-angle value for the subsequent octants_cover_sphere verification.
why it matters
This definition feeds the octants_cover_sphere theorem that confirms 8 × (π/2) = 4π. It supplies the geometric averaging factor required by Conjecture C8 in the module derivation chain, linking the eight-tick octave (T7) to the 1/π term that yields λ_rec = ℓ_P / √π. It closes the discrete-to-continuous step from the 8-face Q₃ geometry to the continuous solid angle in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.