OptimalRungSpec
plain-language theorem explainer
OptimalRungSpec defines the condition for an integer k_opt to maximize critical temperature T_c over phi-ladder rungs in phonon resonance models. Materials researchers screening hydride superconductors cite it when reducing composition search to single-parameter integer choice. The declaration is a direct definition that encodes optimality via universal quantification over all candidate rungs.
Claim. Let $T_c : {k}mapsto T_c(k)$ map rung indices to critical temperatures. The integer $k_{opt}$ is optimal when $T_c(k) leq T_c(k_{opt})$ for every integer $k$.
background
In the phi-ladder phonon resonance setting, lattice frequencies satisfy omega_p = omega_0 * phi^k for integer k, with the single-parameter optimization being the choice of rung index k. The module treats T_c as a function of this index and supplies the optimality predicate for any finite candidate set. Upstream rung definitions appear in Constants (rung := 1) and AnchorPolicy (sector-dependent integer assignment), but here rung simply indexes the discrete phi-multiples.
proof idea
The declaration is a definition whose body is the direct statement forall k, T_c k <= T_c k_opt. No lemmas or tactics are invoked; the Prop is the primitive characterization of the maximizer.
why it matters
The definition supplies the optimization predicate used by the module's phonon resonance claims, which back RS_PAT_008 (SC Screening Platform) and RS_PAT_009. It aligns with the self-similar fixed point phi (T6) and the eight-tick octave structure by reducing material tuning to integer rung selection on the ladder. It leaves per-material omega_0 calibration as an open hypothesis-grade input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.