theorem proved tactic proof

`face_solid_angle_sum`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 145theorem face_solid_angle_sum :
 146    (cube_faces D : ℝ) * per_face_solid_angle = 4 * Real.pi := by

proof body

Tactic-mode proof.

 147  have h6 : (cube_faces D : ℝ) = 6 := by exact_mod_cast faces_at_D3
 148  rw [per_face_solid_angle_eq, h6]; ring
 149
 150/-! ## Part 4: Geometric Seed Assembly -/
 151
 152/-- The geometric seed factor is the passive edge count.
 153    This is WHERE THE 11 COMES FROM. -/

depends on (11)

Lean names referenced from this declaration's body.

cube_faces in IndisputableMonolith.Constants.AlphaDerivation decl_use
faces_at_D3 in IndisputableMonolith.Constants.AlphaDerivation decl_use
per_face_solid_angle in IndisputableMonolith.Constants.AlphaDerivation decl_use
per_face_solid_angle_eq in IndisputableMonolith.Constants.AlphaDerivation decl_use
cube_faces in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
faces_at_D3 in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
cube_faces in IndisputableMonolith.Physics.PMNSCorrections decl_use