anomalousTransportCert
plain-language theorem explainer
anomalousTransportCert assembles the concrete certificate for five anomalous diffusion regimes derived from J-cost, with the ballistic mean-squared-displacement exponent fixed at 2. A statistical mechanician or condensed-matter theorist would cite it when invoking the complete set of subdiffusive through Lévy regimes in the Recognition Science transport analysis. The definition is a direct record construction that supplies the two required fields from the upstream cardinality decision and the reflexivity equality.
Claim. The anomalous transport certificate is the structure asserting that the finite type of diffusion regimes has cardinality 5 and that the ballistic exponent equals 2, witnessed by the explicit cardinality theorem and the reflexivity proof that the exponent is 2.
background
The module derives five canonical anomalous-diffusion regimes for configDim D = 5: subdiffusion (α < 1), normal diffusion (α = 1), superdiffusion (α > 1), ballistic (α = 2), and Lévy flight. The structure AnomalousTransportCert packages exactly these two statements: Fintype.card DiffusionRegime = 5 together with ballisticExponent = 2. This construction sits inside the physics layer that obtains transport exponents from the J-cost functional equation of Recognition Science.
proof idea
The definition is a direct record construction. It populates the five_regimes field by the theorem diffusionRegime_count (a decide tactic that computes the cardinality) and the ballistic_exp field by ballistic_eq_two (a reflexivity proof). No further tactics or reductions are applied.
why it matters
This definition supplies the bundled certificate that the J-cost framework produces exactly five transport regimes with ballistic exponent 2. It completes the local claim inside the AnomalousTransportFromJCost module and aligns with the Recognition Science derivation of stat mech from the functional equation and the phi-ladder. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.