Physics Solid State Physics From Rs

The five phenomena

Solid state physics is the study of rigid matter: how atoms locked in a crystal lattice give rise to electrical conduction, heat capacity, magnetism, and the strange zero-resistance state of superconductivity. The subject's classical core is a handful of canonical phenomena. Band structure explains why some crystals conduct electricity and others insulate. Phonons are quantized lattice vibrations that carry heat. Magnetism covers ferromagnets and their cousins. Superconductivity is the loss of all electrical resistance below a critical temperature. Topology describes phases of matter that are stable to local defects, like the quantum Hall effect. These five are the standard pillars of a solid state course.

In Recognition Science, the framework models solid state physics by identifying these five phenomena as a complete set. Its machine-checked library of formal theorems defines an inductive type with exactly five constructors, one for each phenomenon, and proves the count: five phenomena, no more. The framework then links the crystal lattice to an eight-vertex cube, Q₃, and the first Brillouin zone of a cubic lattice to eight k-points, which is 2 cubed. The band gap, the energy range electrons cannot occupy, is modeled on a phi-ladder: ΔE = φ^k × ℏω, where φ is the golden ratio and ℏω a phonon energy. The module certifies both counts, five phenomena and eight k-points, in a structure with zero axioms and zero sorries.

The concrete payoff is a counting argument. The framework derives that three spatial dimensions force eight k-points, matching the eight corners of a cube. That same eight appears as 2 to the power 3, and the five phenomena sit alongside it as a separate certified count. The module does not derive any material property, such as a specific band gap in electron volts or a critical temperature. It establishes a structural correspondence: the discrete ledger of recognition events, with its eight-tick cycle, mirrors the eight k-points of a cubic lattice, and the five canonical phenomena are the complete set the framework recognizes.

What changes is the framing. A student who learns solid state physics as five separate topics, each with its own equations, can see them as one family under the framework's counting. The five phenomena are not an arbitrary list; they are the full inventory the framework's cost function allows. The eight k-points are not a coincidence of cubic symmetry; they are the same eight that fall out of the framework's dimensional forcing. The module is a bridge: it takes the standard textbook list and shows it fits the framework's discrete structure, without claiming to derive any measured material constant.

theorem solidStatePhenomenonCount : Fintype.card SolidStatePhenomenon = 5 := by decide

theorem brillouinKPoints_8 : brillouinKPoints = 8 := by decide

noncomputable def bandGap (k : ℕ) : ℝ := phi ^ k

What this page does not claim

The module does not derive any measured material property such as a band gap in electron volts or a superconducting critical temperature. The five phenomena are not claimed to be exhaustive in conventional physics, which also studies defects, optical properties, and transport phenomena. The phi-ladder band gap formula is a definitional model, not a theorem about real crystals.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/SolidStatePhysicsFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: