pith. machine review for the scientific record. sign in
theorem proved term proof

geometric_seed_eq

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 166theorem geometric_seed_eq : geometric_seed = 4 * Real.pi * 11 := by

proof body

Term-mode proof.

 167  unfold geometric_seed
 168  rw [solid_angle_Q3_eq]
 169  simp only [geometric_seed_factor_eq_11, Nat.cast_ofNat]
 170
 171/-- The alpha seed factorizes into solid angle × passive channels,
 172    both derived from Q₃ cube geometry with zero imported constants. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.