solidStatePhysicsCert
plain-language theorem explainer
solidStatePhysicsCert packages the two decidable facts that exactly five solid-state phenomena exist and that a cubic lattice has eight Brillouin-zone k-points into the SolidStatePhysicsCert structure. A condensed-matter theorist working inside the Recognition Science derivation would cite it to confirm the match between configDim D=5 and the 2^3 k-point count. The construction is a direct field assignment from the two upstream decidable theorems.
Claim. The structure SolidStatePhysicsCert holds when the cardinality of the type of solid-state phenomena equals 5 and the number of Brillouin-zone k-points for the cubic lattice equals 8.
background
In the Recognition Science treatment of solid-state physics the crystal lattice is identified with the 8-vertex cube Q₃. The module states that the five canonical phenomena (band structure, phonons, magnetism, superconductivity, topology) correspond to configDim D=5, while the first Brillouin zone of a cubic lattice contains 2^D=8 k-points. The upstream theorem solidStatePhenomenonCount establishes Fintype.card SolidStatePhenomenon=5 by decision; the companion theorem brillouinKPoints_8 establishes brillouinKPoints=8 by decision.
proof idea
The definition constructs an instance of the SolidStatePhysicsCert structure by direct field assignment: five_phenomena receives the value of solidStatePhenomenonCount and eight_kpoints receives the value of brillouinKPoints_8.
why it matters
This definition supplies the concrete certificate that closes the B10 Materials section. It records the dimensional consistency between configDim D=5 and the eight-tick octave (2^3 k-points) that follows from T8 (D=3 spatial dimensions). The certificate is available for any later theorem that needs to invoke the solid-state content of Recognition Science without re-proving the two cardinalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.