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)
59theorem robotic_has_6 : HasCubeFaceCount RoboticDOF := by
proof body
Term-mode proof.
60 unfold HasCubeFaceCount; decide
61
62/-- The cube-face identity: 6 = 2 × 3 = face-binary × spatial-dim. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
HasCubeFaceCount
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
RoboticDOF
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
dim
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use