SensorModalitiesCert
plain-language theorem explainer
The SensorModalitiesCert structure certifies that the finite type of robotic sensor modalities has cardinality exactly five. Researchers applying Recognition Science to robotics would cite it to fix the canonical sensor set at configDim D = 5. The definition consists of a single field that directly encodes the cardinality assertion via the Fintype instance on the enumerated modalities.
Claim. A certificate structure whose sole field asserts that the finite type consisting of the five sensor modalities (vision, lidar, radar, tactile, proprioceptive) has cardinality 5.
background
The Robotics.SensorModalitiesFromConfigDim module defines five canonical robotic sensor modalities that correspond to configDim D = 5. These map respectively to external geometry sensing, active ranging, long-range motion detection, contact sensing, and internal body-state sensing. The upstream SensorModality inductive type enumerates precisely these five cases and derives the Fintype instance needed for cardinality statements.
proof idea
This is a structure definition introducing a certificate type with one field that requires the cardinality of the sensor-modality finite type to equal 5. It functions as a direct packaging of the Fintype.card fact for use by the downstream constructor that supplies the concrete value.
why it matters
The structure supplies the type instantiated by sensorModalitiesCert, anchoring the robotics layer of the framework to a fixed sensor count of five. It aligns with the module's derivation of modalities from configDim while remaining consistent with the broader Recognition Science reduction to three spatial dimensions. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.