  95def fragilityMin : ℝ := 16
  96
  97/-- Upper bound on fragility index (polymer-like). -/
  98def fragilityMax : ℝ := 200
  99
 100/-- Strong glass fragility range. -/
 101def isStrongGlass (m : ℝ) : Prop := fragilityMin ≤ m ∧ m ≤ 30
 102
 103/-- Fragile glass fragility range. -/
 104def isFragileGlass (m : ℝ) : Prop := 100 ≤ m ∧ m ≤ fragilityMax
 105
 106/-! ## φ-Scaling of Relaxation Time
 107
 108The relaxation time τ scales as:
 109  τ = τ₀ × φ^n
 110
 111where n depends on temperature relative to Tg.
 112-/
 113
 114/-- Relaxation time scaling with φ. -/
 115def relaxationTime (τ₀ : ℝ) (n : ℕ) : ℝ := τ₀ * Constants.phi ^ n
 116
 117/-- Relaxation time is positive. -/
 118theorem relaxation_pos (τ₀ : ℝ) (hτ : 0 < τ₀) (n : ℕ) :
 119    0 < relaxationTime τ₀ n := by
 120  dsimp [relaxationTime]
 121  apply mul_pos hτ
 122  exact pow_pos Constants.phi_pos n
 123
 124/-! ## Falsification Criteria
 125
 126The glass transition derivation is falsifiable:
 127
 1281. **Kauzmann ratio**: If Tg/Tm deviates significantly from 2/3

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.