totalPhases_eq_10
plain-language theorem explainer
The equality asserts that the total count of condensed matter phases equals 10. Modelers of RS phase structure cite it when assembling the phase certificate that records five matter phases plus five topological phases. The proof is a direct decide tactic that evaluates the sum of the two finite cardinalities.
Claim. The total number of phases, defined as the sum of the cardinalities of the canonical matter phases and the topological phases, equals 10.
background
The module sets five canonical condensed matter phases (solid, liquid, gas, plasma, BEC) equal to configuration dimension 5 and five topological phases (trivial, topological insulator, topological superconductor, Chern insulator, quantum spin liquid) equal to another copy of dimension 5. Their sum is therefore 10, or twice the configuration dimension. The upstream definition states: Total phases: 5 + 5 = 10 = 2 × D, implemented as the natural-number sum of Fintype.card MatterPhase and Fintype.card TopologicalPhase.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality totalPhaseCount = 10. The tactic evaluates the finite cardinalities in the definition of totalPhaseCount and confirms the numerical result.
why it matters
The theorem supplies the total_10 field required by the downstream CondensedMatterPhaseCert definition, which packages the phase counts together with a phase threshold. It realizes the module statement that five matter phases plus five topological phases equal 10 = 2 × configDim D. No open questions or scaffolding remain in the supplied results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.