EntanglementRegime
plain-language theorem explainer
EntanglementRegime enumerates the five canonical regimes of entanglement entropy scaling in quantum many-body systems. Researchers classifying ground states or excited phases under area laws cite this enumeration when partitioning configuration space. The declaration is a direct inductive type with five constructors that derives decidable equality and finiteness automatically.
Claim. An inductive type whose five constructors are the gapped ground state, the critical $(1+1)$-dimensional conformal field theory, topological order, many-body localized states, and thermalizing systems.
background
The module Quantum Entanglement Entropy Area Law treats entanglement entropy through five canonical regimes fixed by configuration dimension D=5. These regimes are the gapped ground state, critical 1+1 CFT, topological order, many-body localized, and thermalizing; each produces a distinct scaling of entanglement entropy with subsystem size. The inductive definition supplies the finite set required for subsequent cardinality statements.
proof idea
The declaration is an inductive definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype in a single line.
why it matters
This definition supplies the enumeration required by the structure EntanglementAreaLawCert, which asserts that the cardinality is exactly five, and by the theorem entanglementRegime_count that proves the count by decision. It anchors the five-regime classification central to the area-law analysis, matching the five canonical regimes stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.