criticalTemp
plain-language theorem explainer
The definition assigns critical temperature T_c on the phi-ladder to phi raised to rung index k in RS units. Materials physicists modeling cuprate and related high-T_c families cite this scaling to link transition temperatures to phonon rung frequencies. It is introduced by direct assignment with no lemmas or reductions.
Claim. The critical temperature on the phi-ladder is given by $T_c(k) = phi^k$ for rung index $k$ in the natural numbers.
background
The module develops high-T_c superconductor transitions from phi-ladder phonon screening. The RS prediction states that T_c times phonon lifetime approximates phi^k for integer rung k. For cuprates such as YBa2Cu3O7, T_c is near 93 K with tau_phonon at phi^{-12} in RS units. The J-cost of phonon coupling lies in the canonical band (0.11, 0.13) for known high-T_c materials, and five families correspond to configuration dimension 5.
proof idea
Direct definition with no proof body. criticalTemp k is set equal to phi ^ k by assignment.
why it matters
This definition supplies the temperature scale for the HighTcCert structure, which certifies five high-T_c families together with the monotonicity property and equilibrium phonon coupling. It also populates the criticalTemp case in the BCSParameter inductive type. The assignment implements the phi-ladder prediction from the module setting and connects to the self-similar fixed point phi in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.