Chemistry Superconducting Tc Cuprate Gt Conventional

The cuprate comparison

Superconductors are materials that carry electric current with zero resistance below a critical temperature, Tc. The cuprates, ceramic compounds containing copper and oxygen, hold the record for the highest Tc at ordinary pressures, around 90 to 130 kelvin. Conventional superconductors, such as aluminum, lead, and niobium, work only below about 30 kelvin and are explained by the BCS theory, in which electrons pair up through vibrations of the crystal lattice, phonons. The cuprates do not fit that picture; their pairing mechanism is still debated.

In Recognition Science, the framework models the energy gap that binds electron pairs as scaling with the golden ratio, phi, roughly 1.618. The framework places superconductor families on a ladder of steps, with a lower step number meaning a higher Tc. The machine-checked library of formal theorems proves that the cuprate family sits at step 3 and the conventional family at step 6, and that a smaller step number gives a strictly larger Tc. The theorem cuprate_gt_conventional states this ordering: the framework's model for cuprates gives a higher critical temperature than its model for conventional superconductors. The same library proves the ratio of the two Tc values is phi cubed, about 4.236, and that iron-based and magnesium diboride families fall between the two extremes.

The framework's library also derives a proxy for the BCS ratio, the dimensionless number relating the energy gap to Tc. The standard weak-coupling BCS value is about 1.76. The framework's expression, 2 times the natural logarithm of phi plus 1, evaluates to about 1.96, and the library proves this number lies between 1.7 and 2.1. The framework presents this as an approximation in the right ballpark, not as an exact match to the measured constant.

What the declaration does not claim is just as important. The theorem proves an ordering inside the framework's own definitions; it does not prove that real cuprates have a higher Tc than real conventional superconductors, which is a measured fact of materials science. The assignment of ladder steps to families is a definitional choice, a model, not a derivation from the framework's axioms. The physical reason why cuprates sit at step 3, or why the golden ratio should set pairing energies, remains open. The framework's claim is that, once you accept the ladder model, the ordering follows by pure arithmetic.

/-- Cuprates have higher Tc than conventional superconductors. -/
theorem cuprate_gt_conventional :
    tcFamily .cuprate > tcFamily .conventional := by
  dsimp [tcFamily, familyLadderStep]
  exact tc_scaling 3 6 (by norm_num)

/-- Ratio between cuprate and conventional Tc follows φ^3.
    (1/φ)^3 / (1/φ)^6 = φ^6 / φ^3 = φ^3 -/
theorem cuprate_conventional_ratio :
    tcFamily .cuprate / tcFamily .conventional = Constants.phi ^ 3 := by
  dsimp [tcFamily, tc_phonon, familyLadderStep]
  -- (1/φ)^3 / (1/φ)^6 = φ^6/φ^3 = φ^3
  have hφpos : 0 < Constants.phi := Constants.phi_pos
  have hφne : Constants.phi ≠ 0 := ne_of_gt hφpos
  have h3 : Constants.phi ^ 3 ≠ 0 := pow_ne_zero 3 hφne
  have h6 : Constants.phi ^ 6 ≠ 0 := pow_ne_zero 6 hφne
  field_simp

/-- The BCS ratio is approximately 1.96 (2*log(φ) + 1).
    log(φ) ≈ 0.481, so 2*log(φ) + 1 ≈ 1.96
    The actual BCS ratio is 2Δ₀/kTc = π/e^γ ≈ 1.764 for weak coupling.
    Our φ-derived approximation is in the right ballpark. -/
theorem bcs_ratio_approx : (1.7 : ℝ) < bcsDeltaTcRatio ∧ bcsDeltaTcRatio < (2.1 : ℝ) := by
  dsimp [bcsDeltaTcRatio]
  -- Use proven bounds from Numerics.Interval.Log: 0.48 < log(φ) < 0.483
  -- Constants.phi = (1 + √5)/2 = Real.goldenRatio
  have h_phi_eq : Constants.phi = Real.goldenRatio := rfl
  rw [h_phi_eq]
  have hlo : (0.48 : ℝ) < Real.log Real.goldenRatio := Numerics.log_phi_gt_048
  have hhi : Real.log Real.goldenRatio < (0.483 : ℝ) := Numerics.log_phi_lt_0483
  constructor
  · -- 1.7 < 2 * log(φ) + 1  ⟺  0.35 < log(φ)
    -- Since 0.48 > 0.35, we have log(φ) > 0.48 > 0.35
    linarith
  · -- 2 * log(φ) + 1 < 2.1  ⟺  log(φ) < 0.55
    -- Since log(φ) < 0.483 < 0.55, we have the result
    linarith

/-- Map superconductor family to φ-ladder step. -/
def familyLadderStep : SuperconductorFamily → ℕ
| .conventional => 6
| .mgb2 => 5
| .ironBased => 4
| .cuprate => 3
| .theoretical => 1

What this page does not claim

The theorem does not prove that real cuprates have a higher Tc than real conventional superconductors. The framework does not derive the measured Tc values of any superconductor family. The framework does not explain why the golden ratio should set pairing energies.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/SuperconductingTc.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: