phi_ladder_optimization_collapses
plain-language theorem explainer
The theorem establishes that the critical temperature computed from the McMillan formula on a finite interval of φ-rungs attains its supremum at one integer rung k_opt. Materials modelers of high-T_c hydrides cite it to justify reducing the search to a single discrete parameter once ω_0 is fixed by hydrogen mass. The proof is a direct term-mode invocation of the Mathlib fact that every nonempty finite set of reals attains its supremum.
Claim. For real numbers ω₀ and λ and positive integer n, there exists an integer k_opt with 0 ≤ k_opt < n such that the critical temperature at φ-rung k_opt equals the supremum of the critical temperatures over rungs 0 through n-1, where the temperature at rung k is given by the McMillan formula with electron-phonon coupling scaled according to the φ-ladder.
background
The module treats hydrogen-dominant superconductors whose bare phonon scale ω₀ is fixed by lattice spring constant and hydrogen mass. The electron-phonon coupling is assumed to follow the φ-ladder λ_k = λ₀ φ^k, so that the only free parameter left in the Eliashberg-McMillan formula is the integer rung k. T_c_phi_rung is defined as phonon_rung(ω₀, k)/1.2 times the exponential of the negative McMillan exponent evaluated at λ and k. The local claim is that this structure collapses the optimization landscape to a discrete search over k.
proof idea
The term proof first constructs the nonempty finite set of candidate rungs via Finset.range n. It then applies the Mathlib lemma Finset.exists_mem_eq_sup' to obtain a witness k_opt inside the set at which the function T_c_phi_rung equals the supremum of the function over the set. The resulting triple is returned directly.
why it matters
The theorem supplies the phi_ladder_collapses clause inside the hydride superconductor optimization master certificate, which aggregates five properties supporting RS_PAT_010. It confirms that the φ-ladder arising from J-uniqueness and the self-similar fixed point reduces a continuous multi-parameter problem to a single integer search, consistent with the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.