sixDOF
plain-language theorem explainer
The declaration assigns the constant six to the degrees of freedom in robotic systems derived from Recognition Science. Engineers modeling autonomous navigation cite it when equating six-DOF control to the six faces of a cube inside J-cost minimization loops. The definition is introduced by direct numerical assignment with no further steps.
Claim. The number of degrees of freedom for a robotic system equals $6$, matching the number of faces on a cube.
background
The Robotics from RS module models five canonical subsystems (sensing, actuation, computation, communication, power) as configDim D = 5. Robot control is a J-cost minimization loop in which autonomous navigation finds paths of minimum cumulative J. Degrees of freedom are fixed at 6-DOF, written as 6 = D + 3 and identified with cube faces, consistent with the forcing chain result that spatial dimension D equals 3.
proof idea
The definition is a direct assignment of the natural number 6.
why it matters
This supplies the six_dof field inside the RoboticsCert structure that certifies both the five subsystems and the six degrees of freedom. It applies the T8 result D = 3 from the unified forcing chain to an engineering setting, closing the link from J-uniqueness and the phi-ladder to practical robotic control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.