GlassRegime
plain-language theorem explainer
GlassRegime enumerates the five canonical regimes of glass-forming liquids in the J-cost model of Recognition Science. Materials physicists working with the Angell fragility index on the phi-ladder would cite this enumeration when certifying the five-regime structure and its scaling properties. The declaration is a direct inductive definition that automatically derives finite cardinality and decidable equality.
Claim. The type of glass regimes is the inductive set consisting of five elements: fragile liquid, strong liquid, supercooled liquid, vitreous solid, and aging glass, equipped with decidable equality and finite cardinality 5.
background
The module models the glass transition with five regimes that correspond to configDim D = 5. The Angell fragility index is defined on the phi-ladder such that the ratio of indices between adjacent regimes equals phi. This inductive type supplies the enumeration required for counting the regimes and for the certification structure that follows.
proof idea
The declaration is an inductive definition introducing five distinct constructors, followed by automatic derivation of the DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This definition supplies the finite set of regimes required by the GlassTransitionCert structure, which asserts cardinality 5 together with phi scaling of fragility indices between adjacent regimes. It anchors the B15-depth analysis of glass transitions, linking directly to the phi-ladder and the configDim = 5 landmark of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.