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

geometric_seed_factor_eq_11

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)

 157theorem geometric_seed_factor_eq_11 : geometric_seed_factor = 11 := by native_decide

proof body

Term-mode proof.

 158
 159/-- The full geometric seed: Ω(∂Q₃) × E_passive.
 160    Both factors derive from Q₃ geometry:
 161    - 4π = Gauss-Bonnet total curvature of ∂Q₃ (Part 3)
 162    - 11 = cube edges − 1 active edge (Part 2) -/

used by (3)

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

depends on (11)

Lean names referenced from this declaration's body.