topologicalPhaseCount
plain-language theorem explainer
The theorem establishes that the Recognition Science model admits exactly five topological phases in the condensed matter sector. Condensed matter theorists working in the RS framework cite this count when enumerating phases governed by recognition winding numbers on the Brillouin zone. The proof is a direct decision procedure on the finite inductive type with its derived Fintype instance.
Claim. The finite set of topological phases has cardinality 5, where the phases are the trivial phase, the $Z_2$ insulator, the $Z$ insulator, the Chern insulator, and the quantum Hall phase.
background
In the Topological Phase Transition from J-Cost module, topological phases are characterised by changes in recognition winding numbers without symmetry breaking. The inductive type TopologicalPhase enumerates five variants (trivial, Z2Insulator, ZInsulator, ChernInsulator, quantumHall) that derive DecidableEq, Repr, BEq and Fintype. The module states that these five phases correspond to configDim D = 5 and that the Kosterlitz-Thouless transition occurs when J(r) crosses the canonical band J(phi) in (0.11, 0.13).
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression. The tactic succeeds because the inductive definition supplies a DecidableEq instance and the type is finite with exactly five constructors.
why it matters
This result supplies the five-phase count to topologicalPhaseCert, which records the transition threshold, and to condensedMatterPhaseCert, which combines it with the five matter phases to obtain total phases = 10 = 2 × D. It fills the topological sector of the RS framework alongside the J-cost function and the eight-tick octave, consistent with the module's claim of zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.