pairingStrength_strictly_increasing
plain-language theorem explainer
The theorem shows that BCS pairing strength on the phi-ladder rises strictly at each integer rung. Materials modelers comparing conventional, intermediate, and strong-coupling superconductors cite it to justify the observed monotonic increase in gap-to-Tc ratios. The short tactic proof rewrites the successor step via the ratio lemma, pulls positivity and the phi > 1.5 bound, then applies a positive-multiplication inequality.
Claim. For every natural number $k$, the pairing strength at rung $k$ satisfies $s(k) < s(k+1)$, where $s(k) := s_0 · φ^k$ and $s_0$ is the reference strength at rung zero.
background
The module treats BCS Cooper-pair binding as a phi-ladder phenomenon. Pairing strength at rung $k$ is defined by $s(k) :=$ referenceStrength $· φ^k$. The module doc states that conventional BCS materials sit at rung 0 with $Δ/T_c ≈ 1.76$, intermediate-coupling at rung 1 with ratio $φ$, and strong-coupling at rung 2 with ratio $φ^2$, extending the same ladder to cuprates and pnictides at rungs 3–4. Upstream, phi_gt_onePointFive supplies the concrete lower bound $φ > 1.5$, while pairingStrength_succ_ratio encodes the exact multiplicative step $s(k+1) = s(k) · φ$ and pairingStrength_pos guarantees positivity.
proof idea
The tactic proof begins by rewriting the goal with pairingStrength_succ_ratio to obtain the inequality $s(k) < s(k) · φ$. It then obtains $0 < s(k)$ from pairingStrength_pos and derives $1 < φ$ from Constants.phi_gt_onePointFive via linarith. The final step applies mul_lt_mul_of_pos_left to the positive factor $s(k)$ and the inequality $1 < φ$, after which simpa closes the goal.
why it matters
This result supplies the strictly_increasing field required by the downstream bcsPairingCert definition, which bundles positivity, the one-step ratio, strict increase, and the adjacent-ratio-equals-phi property into a single certificate. It thereby realizes the module-level claim that dimensionless pairing strength sits on the phi-ladder and increases by exactly $φ$ per rung, consistent with the Recognition Science self-similar fixed point for $φ$. The declaration closes one link in the materials application of the phi-ladder without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.