GlassTransitionCert
plain-language theorem explainer
GlassTransitionCert records that glass transitions admit exactly five regimes whose fragility indices form a geometric sequence with common ratio phi. Condensed-matter modelers of Angell plots cite the structure when mapping J-cost minima onto the observed ladder scaling. The declaration is a plain record type whose three fields are populated by three sibling lemmas in the same module.
Claim. Let $m(k) := phi^k$ denote the fragility index at integer rung $k$. Let GlassRegime be the inductive type with constructors fragileLiquid, strongLiquid, supercooled, vitreous, aging. The certificate asserts that this type has cardinality 5, that $m(k+1)/m(k) = phi$ for every natural number $k$, and that $m(k) > 0$ for all $k$.
background
The module derives glass-transition phenomenology directly from the J-cost functional. GlassRegime is the inductive enumeration of the five canonical regimes (fragile liquid, strong liquid, supercooled, vitreous, aging) that the module equates with configDim D = 5. The fragility index is supplied by the sibling definition fragilityIndex k := phi ^ k, which places every index on the phi-ladder. Upstream, phi enters via the quasicrystal module as the self-similar fixed point of the forcing chain; the companion phi_ratio definition supplies the inverse golden ratio used in energy proxies.
proof idea
The declaration is a structure definition. Its three fields are discharged by the sibling lemmas glassRegime_count, fragility_ratio and fragility_pos; the downstream glassTransitionCert simply assembles those lemmas into an instance of the record.
why it matters
GlassTransitionCert supplies the witness consumed by glassTransitionCert, thereby closing the module's B15 claim that glass transitions exhibit five regimes with adjacent fragility ratios equal to phi. The construction operationalizes the Recognition Science assertion that configDim equals 5 in this materials setting, distinct from the spatial D = 3 obtained in the T8 step of the forcing chain. It also supplies the concrete phi-ladder scaling required by the Angell-index phenomenology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.