solidStatePhenomenonCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the five phenomena from the J-uniqueness or forcing-chain steps T0-T8.
- Does not compute band gaps, phonon spectra, or any dynamical quantities.
- Does not address non-cubic lattices or extensions beyond the listed constructors.
- Does not relate the count to numerical values of alpha, G, or other RS constants.
Lean usage
def solidStatePhysicsCert : SolidStatePhysicsCert where five_phenomena := solidStatePhenomenonCount eight_kpoints := brillouinKPoints_8formal statement (Lean)
27theorem solidStatePhenomenonCount : Fintype.card SolidStatePhenomenon = 5 := by decide
proof body
Term-mode proof.
28
29/-- 8 k-points in Brillouin zone = 2^3. -/