Pith. sign in
module module moderate

IndisputableMonolith.Materials.BCSPairingFromPhiLadder

show as:
view Lean formalization →

Defines BCS pairing strength as a dimensionless sequence on the Recognition Science phi-ladder, normalized so the reference rung has strength 1. Supplies positivity, successive ratios, and strict monotonicity lemmas, plus a certificate bundling those facts. Materials theorists deriving superconducting gap scales from RS rung indices would cite it. The development is mostly definitional with short ratio algebra.

claimReference BCS pairing strength is the RS-native dimensionless constant $1$. Pairing strength at rung $n$ is a positive real sequence on the $\varphi$-ladder with successive ratio fixed by $\varphi$, hence strictly increasing. A certificate packages positivity and the adjacent-ratio identity.

background

Recognition Science places particle and collective scales on a discrete $\varphi$-ladder (golden-ratio self-similar fixed point forced at T6). Dimensionless strengths are pure powers of $\varphi$ relative to a chosen reference rung; absolute units are restored later via the RS yardstick and constants such as $\hbar=\varphi^{-5}$.

This materials module imports only Constants (native tick $\tau_0=1$) and introduces a reference BCS pairing strength equal to the dimensionless unit $1$, together with a rung-indexed pairing strength. The BCS gap and critical temperature in conventional superconductors are proportional to an effective pairing interaction; here that interaction is identified with the ladder value rather than a free Fermi-liquid parameter.

Sibling declarations record positivity, the exact successive ratio, strict increase, and the adjacent-ratio form, then wrap them in a small certificate structure for downstream use.

proof idea

Definition module with short supporting lemmas. referenceStrength is the constant $1$. pairingStrength is defined as a pure $\varphi$-power (or equivalent ladder map) of the rung index. Positivity follows from positivity of $\varphi$. The successive-ratio and adjacent-ratio lemmas are one- or two-line algebraic rewrites of the definition. Strict increase is the ratio lemma plus $\varphi>1$. The certificate is a structure packing those facts; its inhabitant is assembled by applying the lemmas.

why it matters in Recognition Science

Gives the RS-native dimensionless backbone for BCS-type pairing without introducing an extra coupling constant. Downstream materials or condensed-matter developments that need a rung-dependent gap scale, isotope-effect proxies, or pairing hierarchies can import the certificate rather than re-derive ladder arithmetic. No parent theorems are recorded yet in the graph (used_by empty), so the module is a leaf provider for future gap or $T_c$ constructions. It sits in the Materials domain and is consistent with the global $\varphi$-ladder mass/energy formula (yardstick times $\varphi$ to a rung offset).

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)