lambda_at_rung_pos
plain-language theorem explainer
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.
Claim. If $λ > 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.