TopologicalPhase
plain-language theorem explainer
The inductive definition enumerates the five canonical topological phases in Recognition Science as trivial, Z2 insulator, Z insulator, Chern insulator, and quantum Hall. Condensed matter researchers applying the framework to Kosterlitz-Thouless and quantum Hall transitions cite this enumeration to fix the topological sector cardinality at five. The declaration is a direct inductive type with derived Fintype and decidable equality instances that enable immediate cardinality proofs by decision.
Claim. The inductive type of topological phases is defined by the constructors trivial, Z$_2$ insulator, Z insulator, Chern insulator, and quantum Hall, equipped with decidable equality, representation, boolean equality, and finite type structure: $TopologicalPhase := trivial | Z_2Insulator | ZInsulator | ChernInsulator | quantumHall$.
background
In Recognition Science, topological phase transitions are characterized by changes in topological invariants without symmetry breaking and are governed by the recognition winding number on the Brillouin zone. The J-cost function sets the Kosterlitz-Thouless temperature when it crosses the canonical band J(phi) in (0.11, 0.13) for the vortex-antivortex recognition ratio. This module fixes five canonical topological phases corresponding to configuration dimension 5, so that the total phase count (matter plus topological) equals 10 = 2D.
proof idea
The declaration is the inductive definition itself. It introduces the five constructors in one step and derives the DecidableEq, Repr, BEq, and Fintype instances directly, allowing downstream cardinality theorems to discharge by the decide tactic.
why it matters
This enumeration is required by TopologicalPhaseCert, which records Fintype.card TopologicalPhase = 5 together with the transition threshold CanonicalCert. It also feeds topologicalPhaseCount and totalPhaseCount, yielding the 10-phase total that equals twice the configuration dimension. The definition realizes the five topological sectors tied to J-cost transitions and complements the five matter phases in the CondensedMatterPhasesFromRS module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.