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)
107def cubeFaceUniversalityCert : CubeFaceUniversalityCert where
108 quark_6 := quark_has_6
proof body
Definition body.
109 lepton_6 := lepton_has_6
110 cortical_6 := cortical_has_6
111 braak_6 := braak_has_6
112 robotic_6 := robotic_has_6
113 six_equals_2_D := cube_face_identity
114 q3_euler := q3_euler
115 fermion_count := quark_lepton_sum
116 six_cubed := six_cubed
117
118end IndisputableMonolith.CrossDomain.CubeFaceUniversality
depends on (11)
Lean names referenced from this declaration's body.
-
braak_has_6
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
cortical_has_6
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
cube_face_identity
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
CubeFaceUniversalityCert
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
lepton_has_6
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
q3_euler
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
quark_has_6
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
quark_lepton_sum
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
robotic_has_6
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
six_cubed
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
fermion_count
in IndisputableMonolith.Masses.SMVerification
decl_use