ControlArchitecture
plain-language theorem explainer
The inductive definition enumerates five canonical robot control architectures as an inductive type equipped with decidable equality and finite cardinality. Robotics researchers modeling control systems cite it to fix the configuration dimension at five. The definition proceeds by direct enumeration of the five constructors with automatic derivation of the required typeclass instances.
Claim. Let $C$ be the set of robot control architectures. Then $C$ consists of the five elements reactive, deliberative, hybrid, behavior-based, and learning-based, and carries decidable equality together with finite cardinality five.
background
The robotics module classifies control architectures into five canonical types that realize a configuration dimension of five. These types are reactive, deliberative, hybrid, behavior-based, and learning-based. The module supplies this enumeration as a foundational object with no axioms or sorry markers.
proof idea
The declaration is a direct inductive definition listing the five constructors, followed by derivation of DecidableEq, Repr, BEq, and Fintype. No manual tactics appear; the instances are obtained automatically from the inductive structure.
why it matters
This definition supplies the finite set whose cardinality is certified by the downstream theorem controlArchitecture_count and the structure ControlArchitecturesCert. It fixes the dimension at five for robot control architectures. In the Recognition Science framework it provides a concrete instance of dimension fixing, parallel to the spatial dimension three obtained from the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.