theorem other other

`span_down_eq_VF`

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

formal statement (Lean)

 159theorem span_down_eq_VF : (6 + 8 : ℕ) = cube_vertices' 3 + cube_faces' 3 := by native_decide

Lean names referenced from this declaration's body.

cube_faces' in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
cube_vertices' in IndisputableMonolith.Masses.SectorDependentTorsion decl_use