hydride_sc_optimization_one_statement
plain-language theorem explainer
The theorem states that phonon frequencies scale as ω₀ φ^k, the Coulomb pseudopotential satisfies 0 < μ* < 1, and the McMillan critical temperature on any finite rung interval attains its maximum at some integer k_opt. Hydride superconductor theorists would cite this to justify collapsing multi-parameter searches to a single integer rung index. The proof is a direct term that bundles the phonon scaling identity, the numerical bounds on μ*, and the finite-set maximum existence result.
Claim. Let ω₀ > 0 and λ be real numbers and let n > 0 be an integer. The phonon frequency at rung k equals ω₀ φ^k, the pseudopotential satisfies 0 < μ* < 1, and there exists k_opt ∈ {0, …, n−1} such that T_c(ω₀, λ, k) ≤ T_c(ω₀, λ, k_opt) for all k in the interval, where T_c is the McMillan formula evaluated with rung-dependent coupling λ φ^k.
background
The module models hydrogen-dominant superconductors by fixing the bare phonon scale ω₀ = √(K/m_H) and letting the electron-phonon coupling follow the φ-ladder λ_k = λ φ^k. The critical temperature is then given by the McMillan expression T_c(k) = (ω(k)/1.2) exp(−1.04(1+λ_k)/(λ_k − μ*)), with μ* fixed at the standard Eliashberg value 0.1. The phonon rung definition is imported from PhiLadderPhononResonance and supplies the exact scaling ω(k) = ω₀ φ^k. The upstream result T_c_optimization_finite_search proves that any continuous function on a nonempty finite set attains its maximum, here applied directly to the discrete rung index.
proof idea
The term proof constructs a triple: the first component is the constant function returning the phonon scaling identity, the second component packages the two numerical theorems establishing 0 < μ* < 1, and the third component invokes the finite-search theorem T_c_optimization_finite_search on the given interval of length n.
why it matters
This single-statement theorem encapsulates the headline claim of RS_PAT_010 that hydride T_c optimization reduces to an integer search over φ-rungs once ω₀ is fixed. It supplies the structural backing for the module’s headline that the landscape collapses from continuous multi-parameter fitting to discrete rung selection. The result sits inside the Recognition Science forcing chain at the level of material constants and feeds the broader prediction that high-T_c hydrides are governed by the same φ-ladder structure used for mass and coupling constants elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.