module module high

`IndisputableMonolith.Materials.HydrideSCOptimization`

The module supplies parameters for optimizing superconducting transition temperatures in hydrides under the Recognition Science phi-ladder framework. It defines the Coulomb pseudopotential and rung-dependent lambda and Tc expressions for Eliashberg calculations. Materials physicists working on high-Tc hydride predictions would cite these definitions for RS-consistent screening. The module consists of definitions together with simple positivity lemmas.

claimThe Coulomb pseudopotential satisfies $mu^* approx 0.10$ for hydrides. The rung-dependent coupling is $lambda_{rung}$ and the critical temperature is given by the McMillan form $T_c(phi,rung)$ on the phi-ladder.

background

The module sits in the materials track and extends the phi-ladder phonon resonance condition from the upstream PhiLadderPhononResonance module, which supplies Lean backing for RS_PAT_008, RS_PAT_009 and RS_PAT_010. It imports the RS time quantum tau_0 = 1 tick from Constants together with cost functions. Core objects are the Coulomb pseudopotential (standard Eliashberg parameter approximately 0.10 for hydrides), lambda_0, lambda_at_rung, the McMillan exponent, and the phi-ladder Tc optimization functions.

proof idea

This is a definition module, no proofs. It introduces the listed constants and functions with accompanying positivity lemmas such as mu_star_pos and lambda_at_rung_pos.

why it matters in Recognition Science

The module supplies the hydride-specific layer that feeds the SC Screening Platform (RS_PAT_008), SC Compositions (RS_PAT_009) and Hydride SC Optimization (RS_PAT_010). It closes the gap between the general phi-ladder resonance condition and concrete material parameters, using the phi fixed point and eight-tick octave from the forcing chain.

scope and limits

Does not derive the Eliashberg equations from first principles.
Does not specify particular hydride compounds or crystal structures.
Does not compute numerical Tc values for named materials.
Does not treat non-phonon pairing mechanisms.

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