T_c_phi_rung
plain-language theorem explainer
The definition supplies the critical temperature T_c at φ-rung k for a hydride superconductor given bare phonon frequency ω_0 and base coupling λ. Materials researchers optimizing high-T_c hydrides would cite it when reducing the search to a discrete integer parameter. It is realized as the direct McMillan formula with the rung-dependent phonon scale and exponent.
Claim. $T_c(ω_0, λ, k) = (ω_p(k)/1.2) · exp(−m(λ, k))$, where ω_p(k) is the phonon frequency at rung k, λ_k = λ φ^k, and m(λ, k) is the McMillan exponent 1.04(1 + λ_k)/(λ_k − μ*).
background
The hydride model fixes the bare phonon frequency ω_0 = √(K/m_H) from the hydrogen mass and lattice spring constant. The electron-phonon coupling follows the φ-ladder structure λ_k = λ_0 φ^k. The McMillan formula then yields T_c in kelvin once these are substituted. This definition implements the substitution of the rung-dependent phonon scale into the exponential form, with the exponent evaluated at the rung-adjusted coupling. The local setting is the single-parameter optimization of RS_PAT_010, where the landscape collapses from continuous multi-parameter search to discrete search over integer k.
proof idea
This is a one-line definition that evaluates the phonon rung at integer k, divides by 1.2, and multiplies by the exponential of the negated McMillan exponent at the given base coupling λ and rung k. No additional lemmas are applied beyond the imported phonon rung and exponent functions.
why it matters
This definition supplies the explicit T_c expression required by the master certificate HydrideSCOptimizationCert and the collapse theorem phi_ladder_optimization_collapses. It realizes the single-parameter optimization claim of RS_PAT_010. Within the Recognition framework it applies the φ-ladder structure to the materials domain, consistent with discrete tiers and the reduction of continuous parameters to the integer rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.