mu_star
plain-language theorem explainer
mu_star fixes the Coulomb pseudopotential at the constant 0.1 inside the Eliashberg-McMillan Tc formula for hydrogen-dominant superconductors. Materials physicists optimizing high-Tc hydrides cite this fixed value to reduce the search to a single integer phi-rung parameter. The definition is a direct real-number assignment with no lemmas or computation required.
Claim. The Coulomb pseudopotential is the constant $0.1$.
background
The module models hydrogen-dominant superconductors with bare phonon frequency omega_0 = sqrt(K/m_H). The Eliashberg-McMillan Tc formula is Tc(k) = (omega_p(k)/1.2) * exp(-1.04(1+lambda_k)/(lambda_k - mu*)), where lambda_k = lambda_0 * phi^k follows the phi-ladder imported from PhiLadderPhononResonance. mu_star supplies the standard Eliashberg value ~0.10 for hydrides, imported alongside Constants and Cost. The local setting is the single-parameter optimization landscape of RS_PAT_010.
proof idea
Direct constant assignment of the real number 0.1 with no lemmas applied.
why it matters
This definition supplies the fixed mu* required by the master certificate HydrideSCOptimizationCert (clause mu_star_in_band) and the one-statement theorem hydride_sc_optimization_one_statement. It anchors the Eliashberg band condition 0 < mu* < 1 inside the Recognition Science hydride optimization, collapsing the landscape to integer rung selection per the module's phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.