roboticSubsystemCount
plain-language theorem explainer
The declaration proves that the finite type of robotic subsystems has cardinality five, matching the five canonical components required by the Recognition Science robotics model. Engineers constructing RS-derived control architectures would cite this result when verifying subsystem enumeration in autonomous systems. The proof is a one-line wrapper that applies the decide tactic to the derived Fintype instance.
Claim. The finite type consisting of the five robotic subsystems (sensing, actuation, computation, communication, power) has cardinality five: $|RoboticSubsystem| = 5$.
background
The module develops an applied engineering layer in which robot control reduces to J-cost minimization loops and autonomous navigation seeks paths of minimum cumulative J. RoboticSubsystem is the inductive type whose five constructors are sensing, actuation, computation, communication, and power; it derives Fintype, DecidableEq, and related instances. This cardinality statement aligns with the module claim that five subsystems equal configDim D = 5, while six degrees of freedom equal cube faces as D + 3.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic succeeds directly because the inductive definition of RoboticSubsystem derives a Fintype instance, allowing exhaustive enumeration of the five constructors.
why it matters
This theorem supplies the five_subsystems field inside the roboticsCert definition, completing the Lean formalization of the E1 applied engineering layer. It instantiates the Recognition Science assertion that five canonical subsystems arise from configDim D = 5 and supports downstream certification of robotic architectures. The result closes a scaffolding gap without introducing axioms or hidden hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.