lambda_at_rung
plain-language theorem explainer
lambda_at_rung defines the electron-phonon coupling at phi-rung k as the base coupling lambda_0 multiplied by phi to the power k. Hydride superconductor modelers cite it when collapsing the Tc optimization search to a single integer rung parameter in the McMillan formula. It is realized as a direct definition that composes the parameterized base coupling with the phi power.
Claim. The electron-phonon coupling at rung $k$ is $λ(k) = λ_0 · φ^k$, where $λ_0$ is the bare coupling supplied as input and $φ$ is the golden ratio.
background
In the Hydride Superconductor φ-Rung Optimization module the model fixes the bare phonon scale from hydrogen mass and applies the Eliashberg-McMillan formula for Tc. The central assumption is that coupling follows the phi-ladder structure λ_k = λ_0 · φ^k, leaving only the integer rung k as free parameter. The local lambda_0 is defined as the identity on its real argument lam, while the upstream LambdaRecDerivation.lambda_0 supplies the RS balance point 1/√2 and the Constants structure bundles phi together with the abstract CPM constants.
proof idea
Direct definition that applies the local lambda_0 to the input lam and multiplies the result by Constants.phi raised to the power k.
why it matters
This supplies the explicit phi-ladder form of λ_k required by the master certificate HydrideSCOptimizationCert, which asserts that optimization reduces to a discrete search over integer k. It implements the phi-ladder scaling that links to the Recognition Science forcing chain (T5 J-uniqueness and T6 phi fixed point) and feeds the downstream mcmillan_exponent definition together with the positivity theorem lambda_at_rung_pos.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.