solidStatePhenomenonCount
plain-language theorem explainer
The theorem states that the finite type enumerating canonical solid-state phenomena has cardinality five. Materials physicists applying Recognition Science to crystal lattices would cite this to confirm alignment with configDim D. The proof is a direct decision on the inductive definition with five constructors.
Claim. The number of solid-state phenomena is five, where the phenomena are band structure, phonons, magnetism, superconductivity and topology: $5 = |$ {band structure, phonons, magnetism, superconductivity, topology} $|$.
background
The module on Solid State Physics from RS derives solid-state phenomena from the Recognition Science framework, positing five phenomena equal to configDim D. Crystal lattice is modeled as the 8-vertex cube Q₃, with 8 k-points in the Brillouin zone equal to 2^D = 8. The inductive definition lists exactly the five phenomena: band structure, phonons, magnetism, superconductivity, topology.
proof idea
The proof is a term-mode application of the decide tactic, which evaluates Fintype.card directly on the inductive type with five constructors.
why it matters
This supplies the five_phenomena field in solidStatePhysicsCert. It instantiates the module claim that five phenomena equal configDim D=5, consistent with the eight-tick octave (T7) and D=3 spatial dimensions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.