diffusionRegime_count
plain-language theorem explainer
The theorem establishes that the inductive type of anomalous diffusion regimes has cardinality five. Researchers modeling transport phenomena in the Recognition Science framework cite it to confirm the enumeration of subdiffusive, normal, superdiffusive, ballistic, and Lévy-flight cases. The proof is a one-line decision procedure that computes the cardinality directly from the derived Fintype instance on the five constructors.
Claim. The finite set of anomalous diffusion regimes has cardinality $5$, consisting of subdiffusion, normal diffusion, superdiffusion, ballistic motion, and Lévy flight.
background
The module develops anomalous transport from the J-cost functional equation, with five canonical regimes tied to configDim D = 5. DiffusionRegime is the inductive type whose constructors are subdiffusion (α < 1), normal diffusion (α = 1), superdiffusion (α > 1), ballistic (α = 2), and Lévy flight. The module documentation states that mean-squared-displacement exponent α distinguishes these regimes and that the Lean development maintains zero sorry or axiom.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the goal Fintype.card DiffusionRegime = 5, using the automatically derived Fintype instance on the inductive type with exactly five constructors.
why it matters
This supplies the five_regimes component of the AnomalousTransportCert definition, which certifies the complete regime set for J-cost transport. It anchors the stat-mech classification in the module and connects to the five-dimensional configuration space generated by the Recognition Composition Law. The result closes the enumeration step before downstream certification of ballistic exponent α = 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.