TrafficFlowRegime
plain-language theorem explainer
This inductive definition enumerates the five canonical traffic flow regimes that Recognition Science associates with configDim equal to 5. Transportation modelers and physicists working on highway dynamics would cite the type when counting regimes or certifying finite cardinality. The declaration is a direct inductive enumeration that derives DecidableEq, Repr, BEq and Fintype with no additional lemmas.
Claim. The set of traffic flow regimes is the inductive type whose five constructors are free flow, synchronized flow, stop-and-go waves, jammed states, and incident-driven disruptions, equipped with decidable equality and finite cardinality.
background
The module Transportation.TrafficFlowRegimesFromConfigDim treats traffic as a Recognition Science depth whose configuration dimension is fixed at 5. It lists the five canonical dynamical regimes observed in highway-flow modeling: free flow, synchronized flow, stop-and-go waves, jammed states, and incident-driven disruptions. The local setting is given directly by the module header: these regimes are the main ones used in standard highway-flow modeling, with the Lean file containing zero axioms or sorry statements.
proof idea
The declaration is an inductive definition that introduces exactly five constructors, one per regime, and requests the derived instances DecidableEq, Repr, BEq and Fintype. No lemmas or tactics are invoked; the structure is primitive.
why it matters
The type supplies the carrier for the downstream theorem trafficFlowRegime_count, which proves Fintype.card TrafficFlowRegime = 5, and for the certifying structure TrafficFlowRegimesCert. It therefore realizes the explicit claim that traffic regimes number five and match configDim D = 5 inside the Transportation depth of the Recognition Science monolith. No open questions or scaffolding remain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.