CondensedMatterPhasesCert
plain-language theorem explainer
The structure certifies that the inductive enumeration of exotic condensed matter phases has cardinality exactly five when the configuration dimension is five. Condensed matter researchers working inside the Recognition Science program would cite it to fix the phase count for D=5. It is realized directly as a structure whose single field records the Fintype cardinality of the five-constructor inductive type.
Claim. Let $P$ be the inductive type whose constructors are the quantum spin liquid, topological insulator, Weyl semimetal, Mott insulator, and fractional quantum Hall phases. Then the cardinality of $P$ satisfies $|P|=5$.
background
The module CondensedMatterPhasesFromConfigDim enumerates five canonical exotic phases that appear for configuration dimension five. These are the quantum spin liquid, topological insulator, Weyl semimetal, Mott insulator, and fractional quantum Hall effect, each carrying a distinct topological or strong-correlation signature. The structure CondensedMatterPhasesCert packages the cardinality statement for this enumeration, resting on the inductive definition of CondensedMatterPhase whose five constructors immediately determine the Fintype cardinality.
proof idea
The declaration is a structure definition whose sole field asserts that the Fintype cardinality of CondensedMatterPhase equals five. This follows at once from the five constructors listed in the inductive definition of CondensedMatterPhase; the downstream definition condensedMatterPhasesCert supplies the concrete witness by invoking condensedMatterPhase_count.
why it matters
The structure supplies the certified phase count that anchors the condensed-matter sector of the Recognition Science framework at configuration dimension five. It is instantiated by condensedMatterPhasesCert and supports further derivations of phase properties inside the physics module. The construction is consistent with the framework's derivation of discrete counts from dimensional parameters, in line with the eight-tick octave and self-similar scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.