glass_transition_from_ledger
plain-language theorem explainer
The declaration defines the glass-transition ledger condition to be identical to the high-Tc superconductivity condition 1 < phi < 2. Condensed-matter modelers in the Recognition framework cite this when linking glass phases to superconducting inputs via the phi range. It is a direct one-line alias with no additional structure or proof steps.
Claim. The glass-transition ledger condition is the proposition $1 < phi < 2$, where $phi$ is the golden ratio.
background
In the CondensedMatter.GlassTransitionStructure module the glass transition is introduced through ledger conditions that inherit directly from the high-Tc superconductivity structure. The upstream definition high_tc_superconductivity_from_ledger states the proposition 1 < phi ∧ phi < 2. This places the local setting inside the Recognition framework where structural inputs for condensed-matter phases are fixed by the same phi bounds that arise from the self-similar fixed point.
proof idea
The definition is a one-line wrapper that directly references the upstream high_tc_superconductivity_from_ledger definition.
why it matters
This definition supplies the structural input for glass_transition_structure and glass_transition_implies_high_tc, both one-line theorems that propagate the phi condition. It connects to the phi-ladder and the eight-tick octave in the forcing chain, where the interval (1,2) for phi determines allowed phase behaviors. It touches the open question of extracting explicit transition temperatures from these ledger conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.