IndisputableMonolith.Robotics.SensorModalitiesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Robot Sensor Modalities from configDim — Robotics Depth
   6
   7Five canonical robotic sensor modalities (= configDim D = 5):
   8  vision, lidar, radar, tactile, proprioceptive.
   9
  10These correspond to external geometry, active ranging, long-range
  11motion sensing, contact sensing, and internal body-state sensing.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Robotics.SensorModalitiesFromConfigDim
  17
  18inductive SensorModality where
  19  | vision
  20  | lidar
  21  | radar
  22  | tactile
  23  | proprioceptive
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem sensorModality_count : Fintype.card SensorModality = 5 := by decide
  27
  28structure SensorModalitiesCert where
  29  five_modalities : Fintype.card SensorModality = 5
  30
  31def sensorModalitiesCert : SensorModalitiesCert where
  32  five_modalities := sensorModality_count
  33
  34end IndisputableMonolith.Robotics.SensorModalitiesFromConfigDim
  35