fragility_one_lt_zero
plain-language theorem explainer
Fragility at the first eight-beat multiple is strictly smaller than at the zeroth multiple, confirming the decay of the proxy with rising structural index k. Physical chemists modeling viscosity divergence in supercooled liquids would cite this to separate strong glasses from fragile ones under phi-scaling. The proof unfolds the definitions then reduces the power inequality to the elementary comparison lemma for bases in (0,1) after invoking the phi > 1.5 bound.
Claim. Let $m(k) := (1/phi)^{8(k+1)}$ denote the dimensionless fragility proxy at the $k$-th eight-beat multiple, where $phi$ is the golden ratio. Then $m(1) < m(0)$, i.e., $(1/phi)^{16} < (1/phi)^8$.
background
The module treats glass transitions via 8-tick relaxation dynamics in Recognition Science. The eight-beat period is the constant natural number 8. Fragility is the real proxy fragility(k) := (1/phi)^{8(k+1)}, which decays with k and classifies glasses as strong (low proxy) or fragile (high proxy) according to departure from Arrhenius behavior near Tg.
proof idea
After dsimp on fragility and eight_beat_period the goal reduces to (1/phi)^16 < (1/phi)^8. The proof obtains phi > 1.5 from the upstream lemma phi_gt_onePointFive, deduces 0 < 1/phi < 1 via div_lt_one and positivity, notes 16 > 8 by norm_num, and closes with pow_lt_pow_right_of_lt_one₀.
why it matters
The inequality supplies the decay property required by the module's fragility classification and supports the predicted universal Kauzmann ratio Tg/Tm ≈ 2/3 together with 8-tick resonance times. It sits inside the T7 eight-tick octave and phi-scaling of the forcing chain, closing one concrete numerical check for the glass-transition proxy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.