Physics Anomalous Transport From Jcost Diffusion Regime

Diffusion regimes

Diffusion is the random spreading of particles, heat, or information through a medium. Normal diffusion, the kind described by Fick's laws and Einstein's 1905 paper on Brownian motion, spreads distance as the square root of time. Anomalous diffusion covers everything else: particles that spread faster or slower than that square root, or that show other statistical quirks. The standard classification recognizes five regimes, named by their mean-squared-displacement exponent α: subdiffusion (α < 1), normal diffusion (α = 1), superdiffusion (α > 1), ballistic (α = 2), and Lévy flight, which has no finite variance at all.

These regimes appear across physics, biology, and finance. Subdiffusion describes tracer particles in crowded cell cytoplasm and charge transport in disordered semiconductors. Superdiffusion and Lévy flights describe animal foraging patterns, turbulent flows, and the spread of contaminants in groundwater. Ballistic motion, where distance grows linearly with time, is the free-flight limit of particles that rarely collide. The names and the exponent thresholds are standard textbook material, independent of any particular theory of where diffusion comes from.

In Recognition Science, the framework's machine-checked library of formal theorems contains a declaration called DiffusionRegime, an inductive type whose five constructors are exactly these five regimes. The library proves, by direct computation, that the type has exactly five elements, and defines the ballistic exponent as 2, proving that equality by reflexivity. A certificate structure bundles these two facts together. The declaration is a classification, not a derivation: it names the five regimes and records their number, but it does not prove that any physical system must exhibit any particular regime.

The library's contribution is organizational. It gives a formal, machine-checked home to the standard five-way classification, so that later theorems about transport can refer to a single shared object rather than ad hoc lists. The proof that there are five regimes is a finite computation, not a physical law. The declaration does not claim that the five regimes are exhaustive for all possible systems, nor that the exponent α fully characterizes every anomalous process, nor that any specific material or experiment falls into one of these classes.

theorem diffusionRegime_count :
    Fintype.card DiffusionRegime = 5 := by decide

theorem ballistic_eq_two : ballisticExponent = 2 := rfl

What this page does not claim

The declaration does not prove that any physical system must exhibit a particular diffusion regime. The five regimes are not claimed to be exhaustive for all possible anomalous transport processes. The exponent α is not claimed to fully characterize every anomalous process.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/AnomalousTransportFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: