condensedMatterPhase_count
plain-language theorem explainer
The declaration asserts that the inductive type enumerating exotic condensed matter phases has exactly five elements. Researchers mapping Recognition Science's configuration dimension to real materials would cite this cardinality when classifying topological and strongly correlated states. The proof proceeds by a single decision tactic that computes the size of the finite type directly from its constructors.
Claim. The cardinality of the set of condensed matter phases is 5, where the phases consist of the quantum spin liquid, the topological insulator, the Weyl semimetal, the Mott insulator, and the fractional quantum Hall state.
background
The module CondensedMatterPhasesFromConfigDim introduces five canonical exotic phases corresponding to configuration dimension D = 5. These are defined inductively as quantum spin liquid, topological insulator, Weyl semimetal, Mott insulator, and fractional quantum Hall, each carrying distinct topological or correlation signatures. The upstream inductive definition provides the finite enumeration from which the cardinality follows immediately.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the inductive type CondensedMatterPhase, which derives Fintype from its five constructors.
why it matters
This result supplies the count used by the downstream definition condensedMatterPhasesCert to certify the five phases. It fills the slot for configDim D = 5 in the Recognition framework, linking the forcing chain's dimensional constraints to condensed matter phenomenology. No open questions are addressed here beyond the enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.