relaxationTime
Relaxation time in the Recognition Science glass transition model scales as base time τ₀ multiplied by the golden ratio phi raised to integer power n. Chemists deriving fragility indices or Kauzmann ratios from 8-tick dynamics would cite this scaling. It is implemented as a direct definition that applies the phi-ladder multiplication without further reduction.
claimThe relaxation time at integer rung $n$ is defined by $τ(n) = τ_0 φ^n$, where $τ_0$ is the base relaxation time and $φ$ is the golden ratio constant.
background
The module treats glass transition as vitrification of a supercooled liquid under 8-tick relaxation dynamics. Fragility measures how rapidly viscosity rises near Tg, with strong glasses (low fragility, e.g., SiO₂) and fragile glasses (high fragility, e.g., polymers) distinguished by deviation from Arrhenius behavior. The RS mechanism ties this to an 8-tick period that sets the fundamental relaxation time and to φ-scaling that produces the departure from simple exponential decay. Upstream, the Constants structure supplies the phi value and its positivity, while the 8-tick octave and phi fixed-point results from the forcing chain supply the scaling law.
proof idea
This is a direct definition that multiplies the supplied base time by the phi-powered term. No lemmas are applied beyond the built-in real multiplication and natural-number exponentiation; the definition simply encodes the phi-ladder rung for relaxation.
why it matters in Recognition Science
The definition supplies the explicit scaling used by the downstream theorem that relaxation times are positive. It implements the CM-004 claim that 8-tick resonance occurs at characteristic relaxation times and connects directly to the eight-tick octave (T7) and the phi self-similar fixed point (T6). It thereby supports the predicted universal Tg/Tm ratio near 2/3 and the correlation of fragility with molecular complexity.
scope and limits
- Does not fix the integer n for any specific material or molecular structure.
- Does not derive the numerical value of the base time τ₀ from microscopic parameters.
- Does not incorporate explicit temperature dependence beyond the phi scaling.
- Does not address non-power-law corrections to the relaxation form.
formal statement (Lean)
115def relaxationTime (τ₀ : ℝ) (n : ℕ) : ℝ := τ₀ * Constants.phi ^ n
proof body
Definition body.
116
117/-- Relaxation time is positive. -/