pairingStrength
plain-language theorem explainer
Pairing strength at rung k equals the reference BCS value of 1 scaled by phi to the power k. Condensed-matter theorists modeling gap-to-Tc ratios across superconductors cite this to place empirical data on the phi-ladder. The definition is a direct algebraic product that immediately supplies the one-step multiplication property used by downstream certificates.
Claim. The dimensionless pairing strength at rung $k$ is defined by $s(k) = 1 · ϕ^k$, where $ϕ$ is the golden ratio and the reference strength at rung 0 is normalized to unity.
background
The module treats the BCS gap-to-Tc ratio as a dimensionless quantity that occupies successive rungs of the phi-ladder. Each rung multiplies the preceding strength by the golden ratio ϕ, the self-similar fixed point forced in the Recognition Science chain. Reference strength is fixed at 1 in RS-native units, so conventional BCS materials sit at rung 0, intermediate-coupling materials at rung 1, and strong-coupling materials at rung 2.
proof idea
One-line definition that sets the value to referenceStrength multiplied by phi raised to the power k, with referenceStrength itself defined as the constant 1.
why it matters
This definition supplies the explicit form required by BCSPairingCert to certify positivity, strict monotonicity, and adjacent ratios exactly equal to phi. It realizes the module prediction that BCS pairing strengths lie on the phi-ladder, reproducing the observed progression from 1.76 through 2.85 to 4.61 across material classes. The construction rests on the self-similar fixed point phi from forcing-chain step T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.