T_c_phi_rung
The definition supplies the critical temperature T_c at φ-rung k for a hydride superconductor given bare phonon frequency ω_0 and base coupling λ. Materials researchers optimizing high-T_c hydrides would cite it when reducing the search to a discrete integer parameter. It is realized as the direct McMillan formula with the rung-dependent phonon scale and exponent.
claim$T_c(ω_0, λ, k) = (ω_p(k)/1.2) · exp(−m(λ, k))$, where ω_p(k) is the phonon frequency at rung k, λ_k = λ φ^k, and m(λ, k) is the McMillan exponent 1.04(1 + λ_k)/(λ_k − μ*).
background
The hydride model fixes the bare phonon frequency ω_0 = √(K/m_H) from the hydrogen mass and lattice spring constant. The electron-phonon coupling follows the φ-ladder structure λ_k = λ_0 φ^k. The McMillan formula then yields T_c in kelvin once these are substituted. This definition implements the substitution of the rung-dependent phonon scale into the exponential form, with the exponent evaluated at the rung-adjusted coupling. The local setting is the single-parameter optimization of RS_PAT_010, where the landscape collapses from continuous multi-parameter search to discrete search over integer k.
proof idea
This is a one-line definition that evaluates the phonon rung at integer k, divides by 1.2, and multiplies by the exponential of the negated McMillan exponent at the given base coupling λ and rung k. No additional lemmas are applied beyond the imported phonon rung and exponent functions.
why it matters in Recognition Science
This definition supplies the explicit T_c expression required by the master certificate HydrideSCOptimizationCert and the collapse theorem phi_ladder_optimization_collapses. It realizes the single-parameter optimization claim of RS_PAT_010. Within the Recognition framework it applies the φ-ladder structure to the materials domain, consistent with discrete tiers and the reduction of continuous parameters to the integer rung.
scope and limits
- Does not derive the phonon rung from microscopic lattice dynamics.
- Does not specify numerical values for the base coupling λ.
- Does not guarantee an optimal rung without the finite-search theorem.
- Does not extend to anharmonic or multi-band corrections.
- Does not predict absolute T_c without measured ω_0.
Lean usage
example (omega_0 lam : ℝ) (k : ℕ) : ℝ := T_c_phi_rung omega_0 lam kformal statement (Lean)
104def T_c_phi_rung (omega_0 lam : ℝ) (k : ℕ) : ℝ :=
proof body
Definition body.
105 phonon_rung omega_0 k / 1.2 * Real.exp (-(mcmillan_exponent lam k))
106
107/-! ## §2. Existence of optimal rung -/
108
109/-- **THEOREM.** On any finite candidate range, an optimal rung
110exists. This is the single-parameter optimization claim of RS_PAT_010. -/