Chemistry Superconducting Tc Cuprate Conventional Ratio

The cuprate ratio

Superconductors are materials that carry electric current with zero resistance below a critical temperature, Tc. Different families of superconductors have very different Tc values: conventional ones such as aluminum and niobium sit below about 30 kelvin, while cuprates such as YBCO reach 90 to 130 kelvin. The ratio between these two families' critical temperatures is the subject of a formal claim in the Recognition Science framework's machine-checked library of formal theorems.

In Recognition Science, the framework models the energy gap that binds Cooper pairs as scaling with powers of the golden ratio φ, about 1.618. It assigns each superconductor family a step on this ladder: conventional superconductors at step 6, cuprates at step 3. The framework's ledger, a discrete record of recognition events, supplies the ladder structure. A proved theorem, cuprate_conventional_ratio, derives that the ratio of the cuprate Tc to the conventional Tc equals φ³, approximately 4.236. This follows from the definition of the ladder and the elementary fact that (1/φ)ⁿ decreases as n increases.

The theorem is a statement about the framework's model, not about measured materials. It proves a relation between two numbers the framework defines, using the framework's own calibration: a reference temperature of 300 kelvin at step 1. The ratio φ³ is a consequence of that model's arithmetic. It does not prove that any real cuprate has a Tc exactly 4.236 times any real conventional superconductor's Tc. Measured cuprate Tc values vary widely with material and pressure, and the conventional family itself spans a range.

The framework also offers a φ-derived approximation for the BCS weak-coupling ratio Δ/Tc, defined as 2·log(φ) + 1, about 1.96. The standard BCS value is about 1.764. The framework's library proves only that its approximation lies between 1.7 and 2.1, a loose band that contains the standard value. This is a definitional choice, not a derivation of the BCS result.

What the theorem changes is the status of the cuprate ratio within the framework: it is no longer a numerical coincidence but a proved consequence of the ladder model. A reader can now ask whether the φ³ ratio matches any measured pair of Tc values, and the framework's answer is that it does not claim such a match. The theorem's force is internal consistency, not empirical prediction.

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

What this page does not claim

The theorem does not claim any measured cuprate Tc equals φ³ times any measured conventional Tc. The framework does not derive the standard BCS ratio 1.764; it only places its own approximation in a band containing that value. The framework does not claim the φ-ladder is a physical law; it is a modeling choice.

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: