Materials Glass Transition From Jcost Fragility Ratio

A ratio on the fragility ladder

The glass transition is the gradual change of a liquid into a rigid, amorphous solid as it cools, a process central to window glass, polymer plastics, and optical fibers. Materials scientists describe a liquid's behavior on this path by its fragility, a measure of how sharply its viscosity responds to temperature near the transition. A "strong" liquid, like silica, changes viscosity gradually; a "fragile" liquid, like many organic polymers, changes it abruptly. The standard scale for this behavior is the Angell fragility index, which ranks liquids from strong to fragile.

In Recognition Science, the framework's machine-checked library of formal theorems models five canonical glass-transition regimes: fragile liquid, strong liquid, supercooled, vitreous, and aging. The framework defines a fragility index on a ladder of powers of the golden ratio, phi, approximately 1.618. The declaration fragility_ratio proves a simple algebraic fact: the ratio of any two adjacent rungs on this ladder is exactly phi. In symbols, if fragilityIndex k is phi raised to the k-th power, then fragilityIndex (k+1) divided by fragilityIndex k equals phi. The proof is a short calculation, and the theorem is checked with zero axioms beyond the standard logical ones.

The framework's library also proves that there are exactly five regimes and that every fragility index is positive. These three facts, five regimes, the phi ratio, and positivity, are bundled into a certificate structure named GlassTransitionCert. The certificate is a formal summary of what the framework currently establishes about the glass transition.

What the declaration does not claim is just as important. The theorem fragility_ratio is a statement about a defined mathematical ladder; it does not assert that real glass-forming liquids must obey this exact spacing. The framework has not yet derived the Angell fragility index from its deeper cost function, nor has it connected the phi ratio to measured viscosity data for any specific material. The physical bridge from the framework's recognition cost to the observed behavior of actual glasses remains open.

noncomputable def fragilityIndex (k : ℕ) : ℝ := phi ^ k

theorem fragility_ratio (k : ℕ) :
    fragilityIndex (k + 1) / fragilityIndex k = phi := by
  unfold fragilityIndex
  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  rw [div_eq_iff hpos.ne', pow_succ]
  ring

theorem glassRegime_count : Fintype.card GlassRegime = 5 := by decide

theorem fragility_pos (k : ℕ) : 0 < fragilityIndex k := pow_pos phi_pos k

What this page does not claim

The theorem does not assert that real glass-forming liquids obey the phi spacing. The framework has not derived the Angell fragility index from its deeper cost function. No connection is made here between the phi ratio and measured viscosity data for any specific material.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Materials/GlassTransitionFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: