module module high

`IndisputableMonolith.Materials.HydrideSCOptimization`

The HydrideSCOptimization module supplies definitions for Eliashberg parameters and critical-temperature functions specialized to hydride superconductors on the phi-ladder. Condensed-matter researchers applying Recognition Science to high-Tc materials would cite these when computing rung-dependent Tc values. The module contains only definitions and elementary positivity statements.

claim$\mu^* \approx 0.10$ (Coulomb pseudopotential), $\lambda_0$ (base electron-phonon coupling), $\lambda(r)$ (rung-dependent coupling), McMillan exponent, and $T_c(\text{rung})$ via the optimized McMillan formula.

background

Recognition Science places superconductivity inside the phi-ladder phonon resonance framework imported from PhiLadderPhononResonance. That module establishes the resonance condition for phonon-mediated pairing. The present module imports the RS time quantum $\tau_0 = 1$ tick from Constants and the J-cost machinery from Cost to specialize the resonance to hydrides.

The Coulomb pseudopotential is fixed at the conventional Eliashberg value $\mu^* \approx 0.10$. Subsequent definitions introduce rung-indexed coupling strengths $\lambda(r)$ and the resulting critical temperature on the phi-ladder.

proof idea

This is a definition module, no proofs. It declares the functions mu_star, lambda_0, lambda_at_rung, mcmillan_exponent, T_c_phi_rung together with the three positivity lemmas mu_star_pos, mu_star_lt_one, lambda_at_rung_pos.

why it matters in Recognition Science

The module supplies the concrete parameter set required by RS_PAT_010 (Hydride SC Optimization) and supports the screening platform of RS_PAT_008. It translates the abstract phi-ladder resonance into hydride-specific inputs for the McMillan formula.

scope and limits

Does not derive the phonon resonance condition.
Does not perform numerical optimization beyond the defined search.
Does not treat non-hydride superconductors.
Does not include experimental data or fitting.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Materials.PhiLadderPhononResonance module_import

declarations in this module (13)

def mu_star L81
theorem mu_star_pos L83
theorem mu_star_lt_one L84
def lambda_0 L88
def lambda_at_rung L91
theorem lambda_at_rung_pos L93
def mcmillan_exponent L100
def T_c_phi_rung L104
theorem T_c_optimization_finite_search L111
theorem phi_ladder_optimization_collapses L124
structure HydrideSCOptimizationCert L145
def hydrideSCOptimizationCert L160
theorem hydride_sc_optimization_one_statement L178