familyLadderStep
plain-language theorem explainer
The definition assigns each superconductor family to a fixed rung on the phi-ladder, with conventional at step 6 and theoretical at step 1. Condensed-matter researchers deriving Tc ratios from Recognition Science would cite it when applying the phi-power scaling to family-specific critical temperatures. It consists of exhaustive case analysis on the five constructors of the SuperconductorFamily inductive type.
Claim. The function mapping superconductor families to phi-ladder steps is defined by conventional maps to 6, MgB2 to 5, iron-based to 4, cuprate to 3, and theoretical to 1.
background
SuperconductorFamily is the inductive classification into conventional BCS phonon-mediated, MgB2 enhanced phonon, iron-based pnictides, cuprate d-wave, and hypothetical room-temperature categories. The phi-ladder supplies energy scales for the Cooper-pair gap Delta via powers of phi, with the eight-tick ledger structure enforcing macroscopic coherence that raises Tc at higher rungs. The module sets Tc proportional to Delta, so family rung differences produce phi-power ratios between observed critical temperatures.
proof idea
Direct definition by exhaustive pattern matching on the five constructors of SuperconductorFamily, returning the constant natural numbers 6, 5, 4, 3, 1 in that order. No lemmas or tactics are applied.
why it matters
This definition supplies the rung numbers consumed by tcFamily to produce relative Tc values, which in turn feed the theorems cuprate_conventional_ratio (equal to phi^3), cuprate_gt_conventional, iron_between, and mgb2_between. It realizes the module's RS mechanism that places families on distinct phi-ladder steps aligned with the eight-tick octave and the T7 coherence requirement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.