mgb2_between
plain-language theorem explainer
The theorem places the predicted critical temperature of MgB2 strictly between the iron-based and conventional families under phi-ladder scaling. Condensed-matter researchers modeling Tc families would cite it to verify the rung ordering 4 < 5 < 6. The proof is a direct two-line application of the tc_scaling lemma after unfolding the family-to-rung map.
Claim. Let $T_c(f)$ be the dimensionless critical temperature for superconductor family $f$ obtained by evaluating the phonon scaling function at the rung assigned to $f$. Then $T_c$ (iron-based) $> T_c$ (MgB$_2$) and $T_c$ (MgB$_2$) $> T_c$ (conventional).
background
The module derives Tc families from the phi-ladder energy scales in Recognition Science. familyLadderStep maps each family to an integer rung: conventional to 6, MgB2 to 5, iron-based to 4. tcFamily then applies the phonon function tc_phonon to that rung, yielding a value proportional to $(1/phi)^n$. The upstream tc_scaling theorem states that if $n_1 < n_2$ then tc_phonon $n_1 >$ tc_phonon $n_2$, because $0 < 1/phi < 1$ makes the power strictly decreasing. Module context treats superconductivity as 8-tick coherence on the ladder, with lower rung number corresponding to higher Tc.
proof idea
The term proof opens with constructor to split the conjunction. Each conjunct is discharged by dsimp on tcFamily and familyLadderStep followed by an exact call to tc_scaling on the concrete rung pairs (4,5) and (5,6), with norm_num supplying the required strict inequality.
why it matters
The declaration fills the MgB2 slot in the family classification of CM-007, confirming that Tc ratios between families follow phi-power ratios. It supports the module's claim that conventional, MgB2 and iron-based families occupy adjacent rungs with the expected ordering. No downstream uses are recorded, leaving open whether the same scaling extends to the cuprate rung or to the McMillan exponent derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.