module module

`IndisputableMonolith.CrossDomain.CubeFaceUniversality`

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

declarations in this module (20)

def HasCubeFaceCount L29
inductive Quark L31
inductive Lepton L35
inductive CorticalLayer L39
inductive BraakStage L43
inductive RoboticDOF L47
theorem quark_has_6 L51
theorem lepton_has_6 L53
theorem cortical_has_6 L55
theorem braak_has_6 L57
theorem robotic_has_6 L59
theorem cube_face_identity L63
theorem q3_euler L66
theorem cube_face_equicardinal L69
theorem quark_lepton_sum L76
theorem fermion_antifermion_total L81
theorem cube_face_cubed L86
theorem six_cubed L94
structure CubeFaceUniversalityCert L96
def cubeFaceUniversalityCert L107