solidStatePhenomenonCount
plain-language theorem explainer
The theorem asserts that the finite type enumerating canonical solid-state phenomena has cardinality exactly five. A condensed-matter theorist working within the Recognition Science lattice model would cite this when confirming that the count matches the configuration dimension. The proof is a one-line term that invokes the decide tactic on the derived Fintype instance.
Claim. The cardinality of the finite type consisting of the five canonical solid-state phenomena is five: $|$band structure, phonons, magnetism, superconductivity, topology$| = 5$.
background
The module Solid State Physics from RS defines an inductive type whose five constructors are bandStructure, phonons, magnetism, superconductivity, and topology; this type automatically derives DecidableEq, Repr, BEq, and Fintype. The module states that these five phenomena equal configDim D = 5, with the crystal lattice modeled as the 8-vertex cube Q₃ and the first Brillouin zone containing 2^D = 8 k-points. The upstream inductive definition supplies the Fintype instance required for the cardinality computation.
proof idea
The proof is a one-line term that applies the decide tactic. Because the inductive type derives Fintype together with DecidableEq and related instances, decide reduces the equality Fintype.card SolidStatePhenomenon = 5 to a decidable computation that returns true.
why it matters
The result supplies the five_phenomena field of solidStatePhysicsCert, which certifies the extraction of solid-state physics from the Recognition framework. It aligns with the eight-tick octave (T7) and the spatial dimension D = 3, where 2^D produces the eight k-points; the count thereby closes the enumeration of phenomena against configDim. No open scaffolding remains for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.