mu_star_lt_one
plain-language theorem explainer
The Coulomb pseudopotential μ* is shown to satisfy μ* < 1. Hydride superconductor theorists optimizing T_c via the McMillan formula cite this to confirm the Eliashberg stability window holds for the conventional value 0.1. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. $μ^* < 1$, where $μ^*$ is the Coulomb pseudopotential fixed at the standard Eliashberg value 0.1 for hydrogen-dominant superconductors.
background
The hydride superconductor module reduces T_c optimization to a single integer φ-rung parameter k. The Eliashberg-McMillan formula reads T_c(k) = (ω_p(k)/1.2) exp(-1.04(1+λ_k)/(λ_k - μ*)), with λ_k = λ_0 φ^k and ω_0 fixed by hydrogen mass. The Coulomb pseudopotential is introduced as the constant def mu_star : ℝ := 0.1, the conventional value for materials such as H₃S and LaH₁₀.
proof idea
The proof is a one-line wrapper that unfolds the definition of mu_star to the literal 0.1 and invokes norm_num to discharge the numerical comparison 0.1 < 1.
why it matters
This supplies the upper bound half of mu_star_in_band inside HydrideSCOptimizationCert, which feeds the one-statement summary theorem hydride_sc_optimization_one_statement. It verifies that the fixed μ* = 0.1 lies inside the open Eliashberg interval (0,1) required for the exponential factor to remain positive when the φ-ladder phonon resonance model is applied to high-T_c hydrides.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.