TopologicalPhaseCert
plain-language theorem explainer
TopologicalPhaseCert packages a statement that the set of topological phases has cardinality exactly 5 together with a CanonicalCert for the J-cost transition threshold. Condensed matter theorists using the Recognition Science framework cite it to certify the five-phase count and the band condition for Kosterlitz-Thouless transitions. The declaration is a structure definition that directly assembles the Fintype cardinality fact with the imported six-clause J-certificate.
Claim. A topological phase certificate consists of a proof that the finite set of topological phases (trivial, Z2 insulator, Z insulator, Chern insulator, quantum Hall) has cardinality 5 together with a canonical J-band certificate satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(ϕ)>0$, $0.11<J(ϕ)<0.13$, and $J(1/ϕ^2)>0$.
background
The module treats topological phase transitions as changes in recognition winding number on the Brillouin zone without symmetry breaking. The local inductive type TopologicalPhase enumerates exactly the five phases trivial, Z2Insulator, ZInsulator, ChernInsulator and quantumHall, matching the module claim that five canonical phases equal configDim D=5. The transition threshold reuses CanonicalCert, the six-clause structure from CanonicalJBand whose doc-comment states it is the canonical certificate reused by domain certs.
proof idea
The declaration is a bare structure definition with empty body. The five_phases field is supplied by the automatically derived Fintype instance on the inductive TopologicalPhase. The transition_threshold field is filled by direct reference to the CanonicalCert structure imported from CanonicalJBand.
why it matters
The structure is instantiated by the downstream topologicalPhaseCert definition that supplies the concrete cardinality and the cert value. It fills the topological sector of the condensed matter phases in the Recognition Science framework, where the KT transition temperature corresponds to J(r) crossing the canonical band J(ϕ)∈(0.11,0.13). It contributes the five-phase count consistent with the module's statement that configDim D=5 governs the topological invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.