highTcFamilyCount
plain-language theorem explainer
The declaration asserts that exactly five families of high-temperature superconductors are enumerated on the phi-ladder. Condensed-matter theorists classifying cuprate and related systems by rung index would cite this count when linking phonon frequencies to observed T_c values. The proof is a one-line decision procedure that exhausts the constructors of the inductive family type.
Claim. The set of canonical high-temperature superconductor families has cardinality five, where the families comprise cuprates, iron-based, nickelates, heavy-fermion, and organic superconductors.
background
In the Recognition Science treatment of high-T_c materials the phi-ladder assigns phonon frequencies to integer rungs, with critical temperature scaling as T_c times phonon lifetime approximately equal to phi to the power k. The module defines the high-Tc family type as the inductive enumeration of the five observed families: cuprates, iron-based, nickelates, heavy-fermion, and organic. This count is stated to equal the configuration dimension D equal to 5. Upstream rung definitions map sectors or fermions to ladder positions and supply the integer indices appearing in mass and coupling formulas.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic computes the cardinality of the Fintype instance automatically derived from the inductive definition of the high-Tc family type, which contains exactly five constructors, and returns the equality to 5.
why it matters
This result supplies the family count to the highTcCert certificate, which bundles it with monotonicity of critical temperature and canonical phonon coupling. It fills the module claim that five families correspond to configuration dimension D equal to 5. Within the framework it connects to the J-uniqueness step and the eight-tick octave, though its immediate parent is the certification of the phi-ladder prediction for T_c.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.