HydrideSCOptimizationCert
plain-language theorem explainer
Materials researchers optimizing high-Tc hydrides cite the HydrideSCOptimizationCert to certify that T_c maximization reduces to choosing the best integer rung k on the phi-ladder when omega_0 is fixed. The structure collects the band condition on mu_star, positivity of the rung-dependent coupling, existence of an optimal k in any finite range, equality of that optimum to the range supremum, and the explicit phonon rung form. Its fields are filled by direct application of the sibling theorems establishing the band, positivity, finite-search max
Claim. The certificate asserts that the Coulomb pseudopotential satisfies $0 < mu^* < 1$, the electron-phonon coupling satisfies $0 < lambda_0 phi^k$ whenever $lambda_0 > 0$, an optimal rung $k_opt$ exists in any finite candidate set such that $T_c(omega_0, lambda_0, k) leq T_c(omega_0, lambda_0, k_opt)$ for all $k$ in the set, that optimum equals the supremum of $T_c$ values over the set, and the phonon frequency at rung $k$ equals $omega_0 phi^k$.
background
In the hydride superconductor model the bare phonon frequency is fixed by hydrogen mass and lattice spring constant. The rung-dependent coupling is defined as lambda(k) = lambda_0 phi^k and the critical temperature follows the McMillan formula T_c(k) = (omega_p(k)/1.2) exp(-1.04(1+lambda(k))/(lambda(k)-mu*)), where omega_p(k) = omega_0 phi^k is imported from the upstream PhiLadderPhononResonance module. The constants bundle supplies the golden-ratio base phi together with the reference omega_0 value.
proof idea
The declaration is a structure definition whose five fields are populated by the sibling theorems mu_star_pos, mu_star_lt_one, lambda_at_rung_pos, T_c_optimization_finite_search, phi_ladder_optimization_collapses, and a reflexivity proof for the phonon import.
why it matters
This certificate supplies the master structure for the hydride SC optimization theorem, directly feeding the construction of hydrideSCOptimizationCert. It realizes the headline claim of RS_PAT_010 that the optimization landscape collapses to a discrete search over integer phi-rungs, consistent with the self-similar fixed point forced in the T6 step of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.