totalPhaseCount
plain-language theorem explainer
The definition computes the total condensed matter phase count by adding the cardinalities of the matter phase and topological phase enumerations. Condensed matter theorists working in Recognition Science would cite it to confirm the phase inventory equals twice the spatial dimension. It is realized as a direct definition summing Fintype.card applications to the two inductive types.
Claim. The total number of condensed matter phases is defined as the sum of the cardinalities of the matter phase set and the topological phase set, $N := |M| + |T|$, where $M$ enumerates solid, liquid, gas, plasma, BEC and $T$ enumerates trivial, topological insulator, topological superconductor, Chern insulator, quantum spin liquid.
background
In the Condensed Matter Phases from RS module, matter phases are defined by the inductive type with constructors solid, liquid, gas, plasma, BEC. Topological phases use the inductive type with constructors trivial, topological insulator, topological superconductor, Chern insulator, quantum spin liquid. Each set has cardinality 5, matching configDim D = 5. Phase transitions arise when the J-cost of an order parameter crosses the canonical band at J(φ). The local setting asserts that the sum is 10, equal to twice the spatial dimension D from the forcing chain. This rests on upstream enumerations of phases in chemistry phase diagrams and topological phase transitions, which use similar but not identical lists of variants.
proof idea
As a definition with no proof body, it is a direct one-line wrapper that applies Fintype.card to the MatterPhase enumeration and to the TopologicalPhase enumeration before adding the results.
why it matters
This supplies the total phase count required by the CondensedMatterPhaseCert structure, which also records the separate counts of 5 for each category and a phase threshold certificate. It is invoked by the theorem establishing equality to 10. Within the framework it instantiates the claim that the phase count is twice the spatial dimension D, consistent with the eight-tick octave and D = 3 from the unified forcing chain. It leaves open the derivation of these specific phase lists from the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.