ControlArchitecturesCert
plain-language theorem explainer
ControlArchitecturesCert packages the assertion that the inductive enumeration of robot control architectures has cardinality exactly five. A robotics modeler working with configuration dimension D would cite this when confirming that a system matches the canonical set of five paradigms. The declaration is a direct structure definition whose single field inherits the Fintype cardinality from the inductive type.
Claim. Let $C$ be the inductive type whose constructors are the five control architectures reactive, deliberative, hybrid, behavior-based, and learning-based. Then ControlArchitecturesCert is the structure whose single field asserts that the finite cardinality of $C$ equals 5.
background
The module formalizes robotics control architectures as a direct consequence of configuration dimension D = 5. It introduces an inductive type whose five constructors enumerate the standard paradigms: reactive, deliberative, hybrid, behavior-based, and learning-based. The derived Fintype instance on this type supplies the cardinality operation used in the structure field.
proof idea
The declaration is a structure definition whose sole field is the equality Fintype.card ControlArchitecture = 5. No lemmas or tactics are invoked; the equality follows immediately from the derived Fintype instance on the five-constructor inductive type.
why it matters
The structure supplies the certified count that is instantiated by the downstream definition controlArchitecturesCert. It records the robotics depth claim that configDim D = 5 produces exactly these five architectures, completing the enumeration required for robot system modeling within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.