relaxation_pos
plain-language theorem explainer
The theorem establishes that relaxation time τ₀ ⋅ φ^n remains strictly positive for any positive base time τ₀ and any natural number n. Chemists working on glass transition models would cite it to guarantee that φ-scaled relaxation stays physically admissible in the 8-tick framework. The proof is a direct term-mode reduction that unfolds the definition and applies the lemmas mul_pos and pow_pos.
Claim. Let $τ_0 > 0$ be a real number and $n ∈ ℕ$. Then $τ_0 ⋅ φ^n > 0$, where $φ$ denotes the golden-ratio constant fixed by the Recognition Science forcing chain.
background
In the GlassTransition module the function relaxationTime is defined by the product τ₀ ⋅ φ^n, implementing the φ-scaling of relaxation dynamics that follows from the 8-tick period. The module derives glass-transition properties from 8-tick relaxation, with fragility defined as (1/φ)^{8(k+1)} that decays universally. Upstream, Constants.phi_pos supplies the strict positivity of φ, while the fragility definition already records that the same positivity propagates to every multiple.
proof idea
The proof proceeds in term mode. It first simplifies the goal by unfolding the definition of relaxationTime, reducing the claim to positivity of the product τ₀ ⋅ φ^n. It then applies the lemma mul_pos to the hypothesis 0 < τ₀ and discharges the remaining subgoal φ^n > 0 by exact application of pow_pos to Constants.phi_pos.
why it matters
The result secures positivity of all relaxation times inside the φ-scaled glass-transition model, thereby supporting the module’s predictions of a universal Kauzmann ratio ≈ 2/3 and the decay of fragility with eight-beat index. It rests on the eight-tick octave (T7) and the self-similar fixed point φ (T6) of the forcing chain. No downstream theorems are recorded, yet the lemma closes a basic consistency requirement for the fragility and kauzmann derivations that share the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.