lambda_at_rung_pos
Positivity of the scaled electron-phonon coupling at any integer rung follows immediately once the base coupling exceeds zero. Hydride superconductor theorists cite the result to keep the McMillan exponent well-defined over the discrete φ-rung search space. The argument is a one-line term proof that unfolds the product definition and invokes the standard positivity of multiplication together with positive powers of the golden-ratio constant.
claimIf $λ > 0$ and $k ∈ ℕ$, then $λ_k > 0$ where $λ_k := λ ⋅ φ^k$ and $φ > 0$ is the self-similar fixed point.
background
The hydride module models high-T_c materials by setting the electron-phonon coupling at rung k to λ_k = λ ⋅ φ^k, with the bare phonon frequency fixed by hydrogen mass. This reduces the T_c optimization to a search over the single integer parameter k inside the McMillan formula. Upstream, λ_0 is fixed at 1/√2 in RS-native units and the positivity of φ is supplied by the constant definition in the core library.
proof idea
The term proof unfolds lambda_at_rung and lambda_0 to expose the product λ ⋅ φ^k, then applies mul_pos to the hypothesis 0 < lam together with pow_pos on the positive constant φ.
why it matters in Recognition Science
The lemma populates the lambda_pos field of HydrideSCOptimizationCert, which certifies that the entire discrete optimization landscape stays positive. It thereby supports the claim that the φ-ladder collapses the multi-parameter search to a finite integer search over rungs, consistent with the self-similar fixed point forced in the Recognition chain.
scope and limits
- Does not fix the numerical value of the base coupling λ.
- Does not derive or prove the McMillan T_c formula itself.
- Does not guarantee existence of an optimal rung.
- Does not bound the admissible range of rungs k.
formal statement (Lean)
93theorem lambda_at_rung_pos {lam : ℝ} (h : 0 < lam) (k : ℕ) :
94 0 < lambda_at_rung lam k := by
proof body
Term-mode proof.
95 unfold lambda_at_rung lambda_0
96 exact mul_pos h (pow_pos Constants.phi_pos k)
97
98/-- The McMillan exponent at rung `k`: `1.04 (1 + λ_k) / (λ_k − μ*)`,
99defined for `λ_k > μ*`. -/