HighTcFamily
plain-language theorem explainer
HighTcFamily enumerates the five canonical families of high-temperature superconductors in the Recognition Science phi-ladder model. Materials researchers cite the enumeration when classifying cuprates, iron-based, nickelates, heavy-fermion, and organic compounds under the claim that their phonon J-cost lies in the narrow band (0.11, 0.13). The declaration is a direct inductive definition whose automatic Fintype derivation immediately supports cardinality statements.
Claim. Let $F$ be the finite set of high-$T_c$ families. Then $F = $ {cuprates, iron-based, nickelates, heavy-fermion, organic}, equipped with the structure of a finite type.
background
The module treats high-$T_c$ superconductivity via phi-ladder phonon screening, which places transition temperatures at discrete phi-rung frequencies. Five families are asserted to exhaust the known phenomenology, supplying the configurational dimension $D=5$ that complements the spatial dimension $D=3$ forced by the eight-tick octave. The J-cost of the phonon coupling is required to sit inside the canonical interval $J(φ) ∈ (0.11, 0.13)$ for every member of the set.
proof idea
Direct inductive definition with five nullary constructors. Derivation clauses for DecidableEq, Repr, BEq, and Fintype are supplied automatically by Lean, so no separate proof body is required.
why it matters
The definition supplies the five_families field of HighTcCert and is counted by highTcFamilyCount. It realizes the RS claim that exactly five families saturate high-$T_c$ behavior under the phi-ladder (RS_PAT_008–010). The construction fixes the configurational dimension at five, closing one side of the high-$T_c$ prediction while leaving the explicit rung-to-$T_c$ map for later lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.