TopologicalPhase
plain-language theorem explainer
The declaration enumerates five topological phases in the Recognition Science treatment of condensed matter. Researchers modeling J-cost driven transitions cite it to fix the topological sector at cardinality five. The inductive construction directly lists the phases and derives decidable equality plus finite type structure.
Claim. Let $T$ be the set whose elements are the trivial phase, the topological insulator, the topological superconductor, the Chern insulator, and the quantum spin liquid.
background
The Condensed Matter Phases from RS module treats five canonical matter phases as configDim $D=5$ and adds five topological phases that likewise equal $D=5$, so that the total reaches $10=2D$. The upstream inductive definition in TopologicalPhaseTransitionFromJCost supplies the parallel enumeration (trivial, Z2Insulator, ZInsulator, ChernInsulator, quantumHall) that supplies the canonical band context for J-cost crossings.
proof idea
The declaration is the inductive definition itself. It lists the five constructors and invokes the deriving clause to obtain DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
This type supplies the five_topological field of CondensedMatterPhaseCert and the input to topologicalPhaseCount, which asserts cardinality five. It completes the phase enumeration required for the RS-derived classification in which total phases equal twice the configuration dimension, consistent with J-cost band crossings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.