topologicalPhaseCount
plain-language theorem explainer
Recognition Science enumerates exactly five topological phases via an inductive type. Condensed matter researchers citing the framework reference this cardinality to confirm that matter phases plus topological phases total ten, equaling twice the configuration dimension. The proof is a one-line wrapper that applies the decide tactic to the derived Fintype instance.
Claim. The finite type of topological phases has cardinality five.
background
The CondensedMatterPhasesFromRS module states that five topological phases match the configuration dimension D equal to five, paralleling the five canonical matter phases. The inductive type TopologicalPhase enumerates trivial, topologicalInsulator, topologicalSC, chernInsulator, and qSL, each deriving DecidableEq and Fintype. This construction mirrors the enumeration in TopologicalPhaseTransitionFromJCost, whose matching count theorem is also proved by decide.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance automatically derived from the inductive definition of TopologicalPhase.
why it matters
This theorem supplies the five_topological component of condensedMatterPhaseCert, which certifies the total phase count of ten. It realizes the module claim that five matter phases plus five topological phases equal 2 times D, consistent with the forcing chain result that D equals three spatial dimensions. The result closes the enumeration step before phase transition thresholds are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.