IndisputableMonolith.Transportation.TrafficFlowRegimesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Traffic Flow Regimes from configDim — Transportation Depth
   6
   7Five canonical traffic-flow regimes (= configDim D = 5):
   8  free flow, synchronized flow, stop-and-go waves, jammed, incident-driven.
   9
  10These are the main dynamical regimes used in highway-flow modeling.
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith.Transportation.TrafficFlowRegimesFromConfigDim
  16
  17inductive TrafficFlowRegime where
  18  | freeFlow
  19  | synchronizedFlow
  20  | stopAndGo
  21  | jammed
  22  | incidentDriven
  23  deriving DecidableEq, Repr, BEq, Fintype
  24
  25theorem trafficFlowRegime_count :
  26    Fintype.card TrafficFlowRegime = 5 := by decide
  27
  28structure TrafficFlowRegimesCert where
  29  five_regimes : Fintype.card TrafficFlowRegime = 5
  30
  31def trafficFlowRegimesCert : TrafficFlowRegimesCert where
  32  five_regimes := trafficFlowRegime_count
  33
  34end IndisputableMonolith.Transportation.TrafficFlowRegimesFromConfigDim
  35