DiffusionRegime
plain-language theorem explainer
DiffusionRegime enumerates the five canonical anomalous-diffusion regimes that arise from J-cost dynamics when the configuration-space dimension equals five. A researcher classifying mean-squared-displacement exponents in stat-mech models would cite this enumeration to label subdiffusive, normal, superdiffusive, ballistic, and Lévy-flight behaviors. The declaration is a direct inductive definition that automatically derives Fintype, DecidableEq, and the remaining type-class instances.
Claim. The diffusion regimes are the five cases distinguished by the mean-squared-displacement exponent α: subdiffusion (α < 1), normal diffusion (α = 1), superdiffusion (α > 1), ballistic motion (α = 2), and Lévy flight.
background
The module treats anomalous transport as a direct consequence of the J-cost functional in five-dimensional configuration space. The mean-squared-displacement exponent α partitions the possible behaviors into the five regimes listed above. No upstream lemmas are required; the inductive type itself supplies the finite set whose cardinality is later certified.
proof idea
The declaration is the inductive definition of the five constructors together with the derived instances for DecidableEq, Repr, BEq, and Fintype; no separate proof body exists.
why it matters
AnomalousTransportCert and diffusionRegime_count both depend on this type: the former records that its cardinality is five and that the ballistic exponent equals two, while the latter proves the cardinality by decision. The five-regime list therefore closes the classification step in the J-cost derivation of transport, matching the framework's assignment of configDim D = 5 to the anomalous-transport sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.