Chemistry Superconducting Tc Tc Scaling

The phi ladder for critical temperatures

Superconductivity is the state in which certain materials carry electric current with zero resistance, below a material-specific critical temperature (Tc). In the standard BCS theory of conventional superconductors, Tc is set by the energy gap, the minimum energy needed to break apart a Cooper pair of electrons. The Recognition Science framework models Tc as a proxy that falls off by a fixed ratio as a family index increases. The proxy is defined as (1/φ)^n, where φ is the golden ratio, approximately 1.618, and n is a nonnegative integer called the ladder step.

The framework's machine-checked library of formal theorems proves the theorem tc_scaling: if one ladder step is smaller than another, the proxy value at the smaller step is strictly larger than the proxy value at the larger step. In plain language, the proxy decreases as the ladder step increases. The proof is elementary and does not depend on any physics; it uses only the fact that a positive number less than one, raised to a larger power, gives a smaller result. The theorem is a statement about a definition, not about any measured material.

The framework then assigns each superconductor family a ladder step. Conventional BCS superconductors sit at step 6, magnesium diboride at step 5, iron-based superconductors at step 4, and cuprates at step 3. A hypothetical room-temperature superconductor sits at step 1. The library proves, as corollaries of tc_scaling, that cuprates have a higher proxy than iron-based materials, that iron-based materials sit above magnesium diboride, and that magnesium diboride sits above conventional superconductors. The ratio of the cuprate proxy to the conventional proxy is proved to equal φ³, about 4.236.

In Recognition Science, this ladder is not a free fit. The framework derives the golden ratio from its forcing chain, which starts from a proved uniqueness theorem for a cost function. The ladder steps are a definitional choice, not a derivation. The reference temperature at step 1 is set to 300 kelvin, calibrated so that step 3 lands near the cuprate scale of 90 to 130 kelvin. The framework also defines a BCS ratio proxy as 2 log φ + 1, about 1.96, and proves it lies between 1.7 and 2.1, which brackets the measured BCS weak-coupling ratio of about 1.76.

What the declaration does not claim is as important as what it proves. The theorem tc_scaling is a purely arithmetic statement about a definition; it does not establish that any real superconductor family has a Tc in the predicted range. The mapping from families to ladder steps is a modeling assumption, not a measured fact. The framework does not claim to derive the measured Tc values of cuprates or iron-based materials; it claims only that its proxy orders the families in the observed direction. The BCS ratio proxy is an approximation in the right ballpark, not an exact derivation of the measured 1.76.

/-- Tc decreases with ladder step: if `n₁ < n₂` then `tc_phonon n₁ > tc_phonon n₂`.
    Since 0 < 1/φ < 1, we have (1/φ)^n₁ > (1/φ)^n₂ when n₁ < n₂.
    The proof is elementary: for 0 < a < 1, a^n is strictly decreasing in n. -/
theorem tc_scaling (n₁ n₂ : Nat) (h : n₁ < n₂) : tc_phonon n₁ > tc_phonon n₂ := by
  dsimp [tc_phonon]
  have hφpos : 0 < Constants.phi := Constants.phi_pos
  have hφ_gt_1 : 1 < Constants.phi := Constants.one_lt_phi
  have ha_pos : 0 < (1 / Constants.phi) := by positivity
  have ha_lt_one : (1 / Constants.phi) < 1 := by
    rw [div_lt_one hφpos]
    exact hφ_gt_1
  -- For 0 < a < 1 and n₁ < n₂, a^n₂ < a^n₁
  exact pow_lt_pow_right_of_lt_one₀ ha_pos ha_lt_one h

/-- 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

/-- 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)

/-- Iron-based superconductors have intermediate Tc. -/
theorem iron_between :
    tcFamily .cuprate > tcFamily .ironBased ∧
    tcFamily .ironBased > tcFamily .conventional := by
  constructor
  · dsimp [tcFamily, familyLadderStep]
    exact tc_scaling 3 4 (by norm_num)
  · dsimp [tcFamily, familyLadderStep]
    exact tc_scaling 4 6 (by norm_num)

/-- MgB2 is between iron-based and conventional. -/
theorem mgb2_between :
    tcFamily .ironBased > tcFamily .mgb2 ∧
    tcFamily .mgb2 > tcFamily .conventional := by
  constructor
  · dsimp [tcFamily, familyLadderStep]
    exact tc_scaling 4 5 (by norm_num)
  · dsimp [tcFamily, familyLadderStep]
    exact tc_scaling 5 6 (by norm_num)

/-- 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

What this page does not claim

The theorem does not establish that any real superconductor family has a critical temperature in the predicted range. The mapping from families to ladder steps is a modeling assumption, not a measured fact. The framework does not derive the measured Tc values of cuprates, iron-based materials, or any other superconductor.

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: