SensorModality
plain-language theorem explainer
The inductive enumeration of five robotic sensor modalities fixes the discrete basis for configDim derivations in the Recognition Science robotics layer. Researchers modeling sensor configurations or proving finite cardinality results would cite this enumeration. The declaration proceeds by explicit listing of the five cases with automatic derivation of equality and finiteness instances.
Claim. The inductive type consisting of five constructors vision, lidar, radar, tactile, and proprioceptive, equipped with decidable equality, representation, boolean equality, and finite type structure.
background
In the robotics module the configuration dimension is fixed at D = 5, with the five modalities corresponding to external geometry, active ranging, long-range motion sensing, contact sensing, and internal body-state sensing. This enumeration supplies the discrete set whose cardinality is later asserted to equal 5. No upstream lemmas are required; the definition stands alone as the foundational type for downstream certification structures.
proof idea
This is a pure inductive definition with five constructors and no computational content. The derived instances for decidable equality, representation, boolean equality, and finite type are generated automatically by the compiler.
why it matters
The definition supplies the type appearing in the SensorModalitiesCert structure, which asserts Fintype.card equals 5, and supports the sensorModality_count theorem proved by decision. It anchors the robotics depth by fixing the modality count to match configDim D = 5, enabling later connections to the forcing chain and phi-ladder in the broader Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.