CondensedMatterPhase
plain-language theorem explainer
CondensedMatterPhase enumerates five exotic condensed matter phases tied to configuration dimension five in the Recognition Science model. A condensed-matter physicist would cite the type when classifying topological or strong-correlation signatures such as spin liquids and fractional Hall states. The declaration is a direct inductive definition whose Fintype instance follows automatically from the finite list of constructors.
Claim. Define the type of condensed matter phases as the inductive type whose constructors are the quantum spin liquid, the topological insulator, the Weyl semimetal, the Mott insulator, and the fractional quantum Hall state.
background
The module Condensed Matter Exotic Phases from configDim associates five canonical exotic phases with configuration dimension D equal to five. These phases carry distinct topological or strong-correlation signatures and are introduced without additional hypotheses. The declaration imports only Mathlib and Constants; no upstream lemmas are required.
proof idea
The declaration is a direct inductive definition that lists the five phases explicitly. No lemmas or tactics are applied; the derived DecidableEq, Repr, BEq, and Fintype instances are generated automatically from the finite constructors.
why it matters
This type supplies the domain for the downstream theorem condensedMatterPhase_count asserting Fintype.card equals five and for the certification structure CondensedMatterPhasesCert. It fills the slot for exotic phases at configDim = 5, linking to the Recognition framework where spatial dimensions are fixed at three while configuration dimensions accommodate condensed-matter phenomena.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.