SolidStatePhysicsCert
plain-language theorem explainer
Physicists deriving solid-state properties from Recognition Science cite this structure to certify that the model contains exactly five phenomena and that the Brillouin zone of the cubic lattice holds eight k-points. It records the match of the enumerated phenomena to configDim D = 5 together with the 2^3 count for k-points. The declaration is a bare structure definition that imports the Fintype cardinality and the power-of-two constant without additional computation.
Claim. The structure asserts two facts: the inductive type enumerating band structure, phonons, magnetism, superconductivity and topology has cardinality 5, and the number of k-points in the first Brillouin zone equals 8 where that number is defined as $2^3$.
background
The module develops solid-state physics from the Recognition Science framework by identifying five canonical phenomena with the configuration dimension D = 5. Crystal lattices are represented as the 8-vertex cube Q₃, and the first Brillouin zone of a cubic lattice contains 2^D = 8 k-points. The upstream definition fixes the k-point count as the natural number 2 raised to the power 3. The inductive type enumerates the five phenomena and derives a Fintype instance, allowing its cardinality to be asserted as 5.
proof idea
This is a structure definition with an empty proof body. One field asserts the cardinality of the enumerated phenomena equals 5, which follows from the inductive construction and its derived Fintype instance. The second field asserts the k-point count equals 8, which holds by the direct definition of that count as 2^3.
why it matters
This structure is the type instantiated by the downstream solidStatePhysicsCert definition. It anchors the B10 Materials section, connecting the five phenomena to configDim D = 5 and the eight k-points to the spatial dimension D = 3 in the forcing chain T8. The construction supports further derivations of band gaps via the phi-ladder in solid-state systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.