Pith. sign in
module module moderate

IndisputableMonolith.Physics.AnomalousTransportFromJCost

show as:
view Lean formalization →

The module derives ballistic transport properties from the J-cost function in Recognition Science, establishing the exponent as exactly two. Condensed-matter and RS-physics researchers cite it when classifying diffusion regimes. The module consists of sibling definitions and a certification object that import the RS time quantum and assemble the transport claim.

claimThe ballistic exponent satisfies $\alpha=2$ for anomalous transport derived from the J-cost, with the certification object AnomalousTransportCert witnessing the regime.

background

The module imports the RS time quantum $\tau_0=1$ tick from IndisputableMonolith.Constants. It introduces DiffusionRegime, ballisticExponent, diffusionRegime_count, ballistic_eq_two, and AnomalousTransportCert to classify transport from the J-cost. The local setting is the physics domain where J-cost produces specific diffusion and ballistic behaviors.

proof idea

This is a definition module, no proofs. The structure assembles the ballistic exponent claim through the listed sibling declarations and the AnomalousTransportCert object.

why it matters in Recognition Science

The module supplies the ballistic-exponent step that larger Recognition Science transport derivations rely on. It connects the J-cost to concrete transport observables in the physics domain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)