glass_univ
plain-language theorem explainer
Fragility, the dimensionless proxy (1/phi) raised to the power 8(k+1), is strictly positive for every natural number k. Researchers modeling supercooled liquids and vitrification in Recognition Science would cite the result to guarantee the proxy never vanishes. The proof is a compact term-mode reduction that simplifies the definitions then applies positivity of powers after invoking phi positivity.
Claim. For every natural number $k$, the fragility at the $k$-th eight-beat multiple satisfies $(1/phi)^{8(k+1)} > 0$, where $phi$ is the golden ratio.
background
The module treats glass transition as the vitrification of a supercooled liquid under 8-tick relaxation dynamics. The eight-beat period is the constant 8; fragility at index $k$ is then defined as $(1/phi)^{8(k+1)}$, a phi-scaled decay that quantifies departure from Arrhenius viscosity growth. The local setting classifies strong glasses (low fragility, e.g., SiO2) versus fragile glasses (high fragility, e.g., polymers) and predicts a universal Kauzmann ratio near 2/3. Upstream, positivity of phi is supplied by the Constants structure in LawOfExistence.
proof idea
The term proof first applies dsimp to unfold fragility and eight_beat_period into the explicit power expression. It obtains 0 < phi from Constants.phi_pos, deduces 0 < 1/phi by div_pos, and finishes by applying pow_pos to the positive base and arbitrary exponent.
why it matters
The theorem guarantees the fragility proxy remains positive for all structure indices, anchoring the universal decay behavior required by the 8-tick octave (T7) and phi-forcing (T6) in the UnifiedForcingChain. It supports downstream claims on relaxation times and the Kauzmann ratio inside the same module, though no explicit parent theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.