 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
 129
 1302. **Fragility universality**: If fragility doesn't decay with k
 131
 1323. **φ-scaling**: If relaxation times don't follow φ^n pattern
 133-/
 134
 135end
 136
 137end GlassTransition
 138end Chemistry
 139end IndisputableMonolith

papers checked against this theorem

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