mu_star
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from first principles or RS forcing chain.
- Does not depend on any upstream lemmas or definitions.
- Does not vary with material, rung, or phonon scale.
Lean usage
theorem mu_star_in_band : 0 < mu_star ∧ mu_star < 1 := ⟨mu_star_pos, mu_star_lt_one⟩formal statement (Lean)
81def mu_star : ℝ := 0.1
proof body
Definition body.
82