ballisticExponent
plain-language theorem explainer
The ballistic exponent is defined as 2 for mean-squared-displacement scaling in the ballistic regime of anomalous transport. Researchers classifying diffusion regimes from J-cost in Recognition Science would cite this constant when enumerating the five regimes. The definition is a direct real-number assignment.
Claim. The ballistic exponent satisfies $α = 2$.
background
The module derives five anomalous-diffusion regimes from the J-cost function, with configDim D = 5. These regimes are subdiffusion (α < 1), normal diffusion (α = 1), superdiffusion (α > 1), ballistic transport (α = 2), and Lévy flight. The mean-squared-displacement exponent α classifies each regime.
proof idea
The declaration is a direct definition that assigns the constant value 2.
why it matters
This supplies the ballistic exponent required by the AnomalousTransportCert structure, which asserts five_regimes and ballistic_exp : ballisticExponent = 2. It also supports the reflexivity proof in ballistic_eq_two. The assignment completes the regime classification in the J-cost model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.