RoboticDOF
plain-language theorem explainer
RoboticDOF enumerates six constructors for the translational and rotational axes of a three-dimensional robotic manipulator. Researchers assembling cross-domain counts in Recognition Science cite it when populating CubeFaceUniversalityCert to exhibit the recurring factor of six. The declaration is a direct inductive enumeration that automatically derives DecidableEq, Repr, BEq, and Fintype.
Claim. Let RoboticDOF be the inductive type whose six constructors are the Cartesian translations $x$, $y$, $z$ and the Euler rotations roll, pitch, yaw.
background
The module establishes cube-face universality by noting that a 3-cube has six faces, equivalently $2$ times the spatial dimension $D=3$. RoboticDOF supplies one concrete six-element type realizing this count, alongside parallel enumerations for quarks, leptons, cortical layers, and Braak stages. The predicate HasCubeFaceCount, used in the downstream certificate, simply checks that a type has cardinality six.
proof idea
The declaration is an inductive definition with six constructors. Derived instances for Fintype and DecidableEq are generated automatically by Lean; no lemmas or tactics are invoked inside the definition itself.
why it matters
RoboticDOF supplies the robotic case required by CubeFaceUniversalityCert and by the theorem robotic_has_6. It thereby contributes one data point to the structural claim that the count six appears across domains precisely because $D=3$, as stated in the module documentation. The entry closes one slot in the cross-domain collection without invoking the forcing chain or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.