`span_up_eq_2E`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.SDGTForcing
domain: Masses
line: 155 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.SDGTForcing on GitHub at line 155.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

cube_edges' IndisputableMonolith.Masses.SectorDependentTorsion

formal source

 152
 153/-! ## Corollary: The spans are cube-geometric -/
 154
 155theorem span_up_eq_2E : (13 + 11 : ℕ) = 2 * cube_edges' 3 := by native_decide
 156theorem span_lepton_eq_W : (11 + 6 : ℕ) = Constants.AlphaDerivation.wallpaper_groups := by
 157  unfold Constants.AlphaDerivation.wallpaper_groups
 158  native_decide
 159theorem span_down_eq_VF : (6 + 8 : ℕ) = cube_vertices' 3 + cube_faces' 3 := by native_decide
 160theorem spans_partition_N3 : (24 + 17 + 14 : ℕ) = N3' 3 := by native_decide
 161
 162end SDGTForcing
 163end Masses
 164end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.