pairingStrength_pos
plain-language theorem explainer
pairingStrength_pos establishes that the BCS pairing strength at rung k on the phi-ladder is strictly positive for every natural number k. Condensed matter theorists modeling superconductors in the Recognition framework would cite it to anchor the base of the ladder structure. The term proof unfolds the definitions to reduce the claim to the positivity of phi to the power k and closes via linear arithmetic.
Claim. For every natural number $k$, the pairing strength at rung $k$ is positive: $0 < 1 · φ^k$, where the pairing strength is defined as the reference value 1 multiplied by $φ$ to the power $k$.
background
The module develops BCS Cooper-pair binding on the phi-ladder, where the dimensionless pairing strength sits at successive rungs scaled by powers of phi. The pairing strength at rung k is defined as referenceStrength times phi to the power k, and referenceStrength is fixed at the dimensionless value 1. This construction draws on the Constants structure from LawOfExistence, which supplies the assertion that phi is positive.
proof idea
The proof unfolds the definitions of pairingStrength and referenceStrength to expose phi to the power k. It invokes pow_pos instantiated with Constants.phi_pos to obtain the fact that 0 < phi^k. The linarith tactic then concludes the target strict inequality.
why it matters
This positivity result is required by bcsPairingCert, which assembles the full certificate for BCS pairing on the phi-ladder, and by the adjacent-ratio and strictly-increasing theorems. It supplies the base case for the module's structural predictions that conventional BCS materials occupy rung 0 while higher-coupling classes occupy rungs scaled by successive powers of phi. The result therefore anchors the Recognition Science material ladder tied to the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.