isFragileGlass
plain-language theorem explainer
The definition classifies a glass as fragile when its fragility index m satisfies 100 ≤ m ≤ 200. Physical chemists modeling supercooled liquids cite this range to separate polymer-like fragile glasses from strong glasses such as SiO2. The classification is a direct definition that applies the upper bound fragilityMax set to 200.
Claim. A glass with fragility index $m$ is fragile when $100 ≤ m ≤ 200$.
background
The module sets glass transition within Recognition Science via 8-tick relaxation dynamics. Fragility quantifies the rapid rise in viscosity near Tg, with strong glasses (SiO2, GeO2) at low values and fragile glasses (o-terphenyl, polymers) at high values. The RS mechanism ties fragility to deviation from Arrhenius behavior through the eight-tick period and φ-scaling of relaxation time τ = τ₀ × φ^n.
proof idea
This is a direct definition that applies the conjunction 100 ≤ m ∧ m ≤ fragilityMax, where fragilityMax is the constant 200 supplied by the sibling declaration.
why it matters
The definition supports fragility classification inside the glass transition model, which predicts a universal Kauzmann ratio ≈ 2/3 and links fragility to molecular complexity. It rests on the eight-tick octave (T7) from the forcing chain and the φ-scaling of relaxation times. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.