isStrongGlass
plain-language theorem explainer
The definition classifies a glass as strong when its fragility index m lies between the RS lower bound of 16 and the conventional cutoff of 30. Condensed-matter researchers modeling supercooled liquids cite this range to separate SiO2-like behavior from polymer-like fragility inside the eight-tick relaxation picture. It is realized as a direct conjunction of the precomputed fragilityMin constant with the fixed upper threshold.
Claim. A glass with fragility index $m$ is strong when $16 ≤ m ≤ 30$, where the lower bound is the RS-derived minimum for SiO₂-like materials.
background
In the Recognition Science treatment of glass transition, fragility quantifies how rapidly viscosity rises near Tg. The upstream definition fragility(k) supplies a dimensionless proxy that decays as $(1/φ)^{8(k+1)}$ for the k-th eight-beat multiple, encoding the universal 8-tick period. fragilityMin fixes the lower edge at 16, corresponding to strong glasses such as SiO₂ and GeO₂. The module states that glass transition properties arise from 8-tick relaxation dynamics with φ-scaling controlling departures from Arrhenius behavior.
proof idea
The definition is a direct conjunction of the two inequalities fragilityMin ≤ m and m ≤ 30, using the constant fragilityMin := 16 already declared in the same module.
why it matters
This definition supplies the classification boundary that separates strong from fragile glasses inside the RS glass-transition model. It operationalizes the distinction drawn in the module between low-fragility (SiO₂) and high-fragility regimes within the eight-tick octave (T7). No downstream theorems yet reference it, leaving open its integration with relaxationTime and the Kauzmann ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.