sensorModality_count
plain-language theorem explainer
The theorem fixes the cardinality of the robotic sensor modality type at five. Robotics modelers building configuration spaces with configDim D = 5 would cite it to lock the modality count. The proof is a one-line decision tactic that enumerates the five inductive constructors.
Claim. The finite type of canonical robotic sensor modalities has cardinality five: $ |S| = 5 $, where $ S $ consists of vision, lidar, radar, tactile and proprioceptive.
background
The module introduces five canonical robotic sensor modalities tied to configDim D = 5. Vision covers external geometry, lidar active ranging, radar long-range motion sensing, tactile contact sensing, and proprioceptive internal body-state sensing. The upstream inductive definition SensorModality enumerates exactly these five cases and derives Fintype, DecidableEq and Repr instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card directly from the inductive constructors of SensorModality.
why it matters
This supplies the five_modalities field inside the SensorModalitiesCert definition, anchoring the robotics depth of the Recognition framework at configDim = 5. It supplies a concrete count that downstream certification can reference without further proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.