strongly_correlated_implies_glass
plain-language theorem explainer
Strong electron correlation encoded in the ledger directly entails the glass transition ledger condition. Condensed matter researchers modeling high-Tc materials would cite this link when connecting correlation effects to glassy structural inputs. The proof is a one-line term that returns the hypothesis, using the definitional identity between the two predicates.
Claim. If the ledger satisfies the strong-correlation condition for electrons, then the glass-transition condition holds.
background
In this condensed matter module the glass transition is introduced as the ledger predicate glass_transition_from_ledger, defined to be identical to the high-Tc superconductivity ledger predicate. The strong-correlation structure is captured by the predicate strongly_correlated_electrons_from_ledger, which is itself defined as equal to the glass transition predicate. The module imports GlassTransitionStructure and places the implication inside the Recognition Science ledger framework for material structure.
proof idea
The proof is a one-line term that returns the hypothesis h directly, which is valid because strongly_correlated_electrons_from_ledger is definitionally equal to glass_transition_from_ledger.
why it matters
The declaration closes a definitional loop that keeps strong-correlation structure consistent with the glass-transition input required for high-Tc and glassy models. It supports the ledger-based derivation of condensed-matter properties without adding new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.