controlArchitecture_count
plain-language theorem explainer
The theorem asserts that the finite set of canonical robot control architectures has cardinality five when configuration dimension equals five. Robotics researchers applying dimensional constraints to control design would cite this result. The proof is a one-line decision procedure on the Fintype instance derived from the five-constructor inductive type.
Claim. The cardinality of the set of canonical robot control architectures (reactive, deliberative, hybrid, behavior-based, learning-based) equals five: $5$.
background
The module defines five canonical robot-control architectures corresponding to configDim D = 5: reactive, deliberative, hybrid, behavior-based, learning-based. These form an inductive type deriving DecidableEq, Repr, BEq, and Fintype. The local setting applies Recognition Science dimensional constraints to robotics control, with the module stating zero sorrys or axioms.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality of Fintype.card of the architecture type with 5, using the derived Fintype instance from the inductive definition.
why it matters
This supplies the five_architectures field inside the controlArchitecturesCert definition. It realizes the module claim that robot control architectures number five at configDim = 5, extending the Recognition Science forcing chain at the dimensional step. No open questions are indicated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.