T_c_optimization_finite_search
plain-language theorem explainer
On any finite interval of candidate phi-rungs, a maximizing rung k_opt exists for the McMillan T_c formula with lambda scaled by phi^k. Hydride superconductor modelers cite it to reduce multi-parameter optimization to a single integer search over rung index. The proof is a one-line wrapper that invokes the finite-set maximum lemma after confirming the range is nonempty from the hypothesis 0 < n.
Claim. Let $0 < n$ be a positive integer and let $omega_0, lambda$ be real numbers. There exists an integer $k_{opt}$ with $0 leq k_{opt} < n$ such that $T_c(omega_0, lambda, k) leq T_c(omega_0, lambda, k_{opt})$ for every integer $k$ with $0 leq k < n$, where $T_c(omega_0, lambda, k)$ is the McMillan critical temperature evaluated at rung $k$ with electron-phonon coupling $lambda cdot phi^k$.
background
The module treats hydrogen-dominant superconductors by fixing the bare phonon scale $omega_0 = sqrt(K/m_H)$ and letting the coupling follow the phi-ladder $lambda_k = lambda_0 cdot phi^k$. The sibling definition T_c_phi_rung implements the McMillan formula as phonon_rung omega_0 k / 1.2 times exp of the negative mcmillan_exponent at that rung. This supplies the single free parameter k once omega_0 is fixed by hydrogen mass and lattice constant, as described in the module header for RS_PAT_010.
proof idea
The proof is a one-line wrapper. It first builds a witness that Finset.range n is nonempty from the hypothesis 0 < n, then applies the library lemma Finset.exists_max_image to the set with the function T_c_phi_rung omega_0 lam.
why it matters
The theorem is invoked inside hydrideSCOptimizationCert to supply the existence witness and inside the one-statement summary hydride_sc_optimization_one_statement. It realizes the single-parameter optimization claim of RS_PAT_010 by showing that the phi-ladder structure collapses the continuous search over omega_p, lambda and mu-star to a discrete integer search over rung index k. This aligns with the Recognition Science reduction from multi-parameter materials models to the phi-ladder fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.