trafficFlowRegimesCert
plain-language theorem explainer
This definition supplies a certificate that the traffic flow model contains exactly five regimes. Transportation modelers working in Recognition Science would cite it to fix configDim at five when simulating highway dynamics. The construction is a one-line wrapper that populates the certificate structure from the decidable cardinality theorem on the regime enumeration.
Claim. Let $R$ be the finite type enumerating the five canonical traffic flow regimes. Define the certificate $C$ by the assertion that the cardinality satisfies $|R| = 5$.
background
The module sets configDim to five to encode the primary dynamical regimes of highway traffic: free flow, synchronized flow, stop-and-go waves, jammed, and incident-driven. These are collected in the inductive type TrafficFlowRegime whose finite cardinality is the sole field of the structure TrafficFlowRegimesCert. The upstream theorem trafficFlowRegime_count proves this cardinality equals five by direct decidable computation.
proof idea
The definition is a one-line wrapper that assigns the five_regimes field of TrafficFlowRegimesCert directly to the value of trafficFlowRegime_count.
why it matters
The definition certifies the fixed regime count required for any transportation model inside Recognition Science. It supplies the concrete instance needed to anchor configDim = 5 in downstream highway-flow calculations. No further open questions are addressed; the module reports zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.