Physics Condensed Matter Phases From Config Dim

Five phases, one dimension

Condensed matter physics studies materials where many particles act together, and some of its most striking discoveries are phases that do not fit the textbook categories of solid, liquid, or gas. Five of these exotic phases are the quantum spin liquid, the topological insulator, the Weyl semimetal, the Mott insulator, and the fractional quantum Hall state. Each has a distinct signature: the quantum spin liquid has no magnetic order even at absolute zero, the topological insulator conducts on its surface but not through its bulk, the Weyl semimetal hosts massless electrons, the Mott insulator blocks conduction despite being partially filled, and the fractional quantum Hall state carries fractions of an electron's charge.

The module in the machine-checked library of formal theorems defines these five phases as a single inductive type, a way of listing all possibilities, and proves that there are exactly five of them. The proof is a direct computation: the type has five constructors, one for each phase, and the theorem Fintype.card confirms the count. The certificate structure bundles this count into a reusable fact. The library reports zero axioms and zero unfinished proofs, meaning the count is fully checked by the kernel.

In Recognition Science, the framework models physical structure from a discrete record of events, and the configuration dimension is the number of independent degrees of freedom in that record. The framework's claim is that these five phases correspond to a configuration dimension of five. This is a definitional choice, not a derivation: the framework chooses to identify the five phases with the five dimensions, and the library formalizes that identification. The count theorem is proved, but the physical correspondence to real materials is a modeling assumption.

The practical consequence is a compact inventory. A reader who wants to know what exotic phases exist can find them listed and counted in one place, with the count machine-checked. The framework contribution is not a new prediction about any single material; it is a structural claim that the variety of phases is not arbitrary but matches a specific number. That claim is honest about its status: the count is a theorem, the correspondence is a model, and the physical bridge to real materials remains open.

inductive CondensedMatterPhase where
  | quantumSpinLiquid
  | topologicalInsulator
  | weylSemimetal
  | mottInsulator
  | fractionalQHall
  deriving DecidableEq, Repr, BEq, Fintype

theorem condensedMatterPhase_count :
    Fintype.card CondensedMatterPhase = 5 := by decide

structure CondensedMatterPhasesCert where
  five_phases : Fintype.card CondensedMatterPhase = 5

def condensedMatterPhasesCert : CondensedMatterPhasesCert where
  five_phases := condensedMatterPhase_count

What this page does not claim

This module does not derive the existence of any real material from first principles. The correspondence between the five phases and configuration dimension five is a modeling choice, not a proved physical law. The module does not predict any new phase beyond the five listed.

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/CondensedMatterPhasesFromConfigDim.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: