topologicalPhaseCert
plain-language theorem explainer
The definition constructs a concrete certificate asserting exactly five topological phases together with a CanonicalCert for the J-cost transition threshold. Condensed matter theorists mapping Kosterlitz-Thouless or quantum Hall transitions to recognition winding numbers would cite this when fixing the phase count to configDim D = 5. The construction is a direct record instantiation that pulls the cardinality from a decidable enumeration and the threshold from an existing cert.
Claim. Let TopologicalPhaseCert be the structure whose fields are the assertion that the set of topological phases has cardinality five together with a CanonicalCert for the transition threshold. The definition supplies the instance in which the cardinality is witnessed by enumeration and the threshold is taken from the canonical band certificate.
background
In the Recognition Science treatment of condensed matter, topological phase transitions are governed by the recognition winding number on the Brillouin zone rather than by symmetry breaking. The module states that five canonical phases (trivial, Z2 insulator, Z insulator, Chern insulator, quantum Hall) correspond to configDim D = 5, with the Kosterlitz-Thouless temperature arising when J(r) crosses the band J(phi) in (0.11, 0.13). This rests on the upstream theorem that the cardinality of the set of topological phases equals five, established by direct decidable enumeration, and on the structure TopologicalPhaseCert that packages the count with a CanonicalCert.
proof idea
The definition is a direct record construction. It assigns the five-phases field the theorem that establishes cardinality five via the decide tactic and assigns the transition-threshold field the value of cert.
why it matters
This definition supplies the concrete certificate required by the topological phase transition framework. It closes the enumeration of five phases (equal to 2 times D) to the J-cost threshold, supporting the mapping of RS constants to observed topological invariants. The construction is consistent with the eight-tick octave and the derivation of D = 3 spatial dimensions extended to the topological sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.