pith. machine review for the scientific record. sign in
def definition def or abbrev high

fragilityMax

show as:
view Lean formalization →

fragilityMax defines the upper bound of 200 on the fragility index for polymer-like glasses in the Recognition Science model. Chemists classifying supercooled liquids near Tg would cite it to mark the fragile regime boundary alongside the lower threshold of 100. The declaration is a direct constant assignment with no reduction steps or lemmas.

claimThe upper bound on the fragility index for polymer-like glasses is defined as $200$.

background

The Chemistry.GlassTransition module models vitrification of supercooled liquids through 8-tick relaxation dynamics. Fragility quantifies the rapid rise in viscosity near Tg, separating strong glasses (SiO₂) from fragile ones (polymers). The upstream fragility definition supplies the dimensionless proxy (1/φ)^(8(k+1)) that decays universally across eight-beat multiples.

proof idea

Direct constant definition that assigns the literal value 200 as the polymer-like ceiling.

why it matters in Recognition Science

The constant supplies the upper endpoint for isFragileGlass, completing the fragile-glass predicate 100 ≤ m ∧ m ≤ fragilityMax. It implements the φ-scaling departure from Arrhenius behavior predicted by the 8-tick period in the glass-transition mechanism and the module's claim that fragility correlates with molecular complexity.

scope and limits

formal statement (Lean)

  98def fragilityMax : ℝ := 200

proof body

Definition body.

  99
 100/-- Strong glass fragility range. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.