entanglementRegime_count
plain-language theorem explainer
The declaration asserts that the finite type of entanglement regimes has cardinality five, matching the five canonical scaling behaviors for entanglement entropy in quantum many-body systems. Physicists classifying phases by area-law properties would cite this count when building certificates for ground-state or thermal entanglement. The proof is a one-line decision procedure that computes the cardinality from the derived Fintype instance on the inductive type.
Claim. The set of entanglement regimes has cardinality five: $ |EntanglementRegime| = 5 $, where the regimes are the gapped ground state, critical 1+1 CFT, topological order, many-body localized, and thermalizing cases.
background
The module defines five canonical area-law regimes for entanglement entropy scaling with subsystem size. The inductive type EntanglementRegime enumerates exactly these cases: gappedGroundState, critical1p1CFT, topologicalOrder, manyBodyLocalized, thermalizing, and derives Fintype, DecidableEq, and related instances. This classification supplies the configDim D = 5 used in the area-law certificate. The upstream result is the inductive definition itself, which directly provides the finite enumeration.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card EntanglementRegime = 5, relying on the automatically generated Fintype instance from the inductive definition of EntanglementRegime.
why it matters
This cardinality is referenced directly by the downstream definition entanglementAreaLawCert to populate the five_regimes field of the area-law certificate. It anchors the module's claim of five distinct regimes, each with its own entanglement-entropy scaling, inside the Recognition Science treatment of quantum physics. The result closes the enumeration step without invoking the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.