mu_star_pos
plain-language theorem explainer
mu_star_pos delivers positivity of the fixed Coulomb pseudopotential at 0.1. Hydride superconductor modelers cite it to confirm the Eliashberg-McMillan inputs lie in the physical band. The proof goes through by unfolding the constant definition and applying numerical normalization.
Claim. The Coulomb pseudopotential satisfies $0 < 0.1$.
background
The Hydride Superconductor φ-Rung Optimization module fixes the bare phonon scale ω_0 from hydrogen mass and lattice spring constant, then applies the Eliashberg-McMillan formula T_c(k) = (ω_p(k)/1.2) exp(-1.04(1+λ_k)/(λ_k - μ*)). Here λ_k follows the φ-ladder λ_k = λ_0 · φ^k, leaving only the integer rung k as free parameter. The sibling definition mu_star sets the Coulomb pseudopotential to the standard hydride value 0.1.
proof idea
The proof is a one-line wrapper that unfolds mu_star to the constant 0.1 and invokes norm_num to verify the inequality.
why it matters
It supplies the lower bound used inside hydrideSCOptimizationCert to certify μ* ∈ (0,1) and inside hydride_sc_optimization_one_statement to bundle the structural facts for RS_PAT_010. The result confirms the Eliashberg band condition required for the φ-ladder to collapse the multi-parameter search to a discrete integer rung search.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.