CondensedMatterPhaseCert
plain-language theorem explainer
The CondensedMatterPhaseCert structure bundles cardinality assertions for five matter phases and five topological phases whose sum equals ten, together with a CanonicalCert witness on the J-band threshold. A condensed-matter theorist mapping RS-derived phase diagrams onto B9/B13 materials would cite the certificate when confirming that the enumerated phases match twice the configuration dimension. The definition simply assembles the Fintype.card facts from the two inductive enumerations with the imported CanonicalCert record.
Claim. A record type asserting that the set of matter phases (solid, liquid, gas, plasma, BEC) has cardinality 5, the set of topological phases (trivial, topological insulator, topological superconductor, Chern insulator, quantum spin liquid) has cardinality 5, their sum equals 10, and that the phase threshold satisfies the CanonicalCert conditions on the J function.
background
The module enumerates matter phases via the inductive type with constructors solid, liquid, gas, plasma, BEC and topological phases via trivial, topologicalInsulator, topologicalSC, chernInsulator, qSL. The local setting states that these two sets of five phases each sum to ten, which equals twice the configuration dimension D, and that transitions occur when J(order parameter) crosses the canonical band J(phi). Upstream CanonicalCert supplies the five-clause record: J(1) = 0, J(x) = J(1/x) for x ≠ 0, J(phi) > 0, the interval bound 0.11 < J(phi) < 0.13, and J(1/phi²) > 0. The sibling totalPhaseCount definition is the sum of the two Fintype.card values.
proof idea
The declaration is a structure definition whose four fields directly record the two cardinality equalities, invoke the totalPhaseCount definition, and embed an instance of CanonicalCert. No tactics or lemmas are applied; the structure simply packages the already-computed facts from the inductive enumerations and the imported certificate.
why it matters
The certificate supplies the phase-count data consumed by the downstream condensedMatterPhaseCert definition. It realizes the module claim that five matter phases plus five topological phases total ten, thereby linking the J-cost formalism and CanonicalCert band condition to the concrete condensed-matter phase diagram. The structure sits at the interface between the Recognition Science forcing chain (T5 J-uniqueness and T6 phi fixed point) and the configDim D = 5 assignment for phase space, distinct from spatial D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.