pith. machine review for the scientific record. sign in
theorem proved term proof high

cuprate_conventional_ratio

show as:
view Lean formalization →

The ratio of phonon-proxy critical temperatures for cuprate and conventional superconductor families equals phi cubed. Condensed matter theorists comparing high-Tc scaling laws would cite this when testing phi-ladder predictions against observed family ratios. The proof is a term-mode reduction that unfolds the ladder-step definitions and applies field simplification after confirming phi positivity.

claimLet $T_c(f)$ denote the phonon-proxy critical temperature for superconductor family $f$, obtained by evaluating $(1/phi)^n$ at the ladder step $n$ assigned to $f$. Then $T_c($cuprate$)/T_c($conventional$) = phi^3$.

background

The module models superconducting Tc via a phi-ladder proxy derived from Recognition Science energy scales. familyLadderStep maps each family to a natural-number rung: cuprate to 3 and conventional to 6. tcFamily(f) is then tc_phonon of that rung, where tc_phonon(n) equals (1/phi)^n. This construction follows the module's RS Mechanism, in which Cooper-pair gaps scale with phi powers and Tc remains proportional to the gap, with conventional BCS occupying higher rungs (lower Tc) than cuprates.

proof idea

The term proof first applies dsimp to unfold tcFamily, tc_phonon, and familyLadderStep, reducing the left-hand side to (1/phi)^3 / (1/phi)^6. It then obtains 0 < phi from Constants.phi_pos, derives phi ≠ 0 and the relevant powers nonzero via ne_of_gt and pow_ne_zero, and concludes with field_simp to reach phi^3.

why it matters in Recognition Science

This result instantiates the module's prediction that Tc ratios between superconductor families follow phi-power ratios, directly supporting the phi-ladder energy scales and 8-tick coherence requirements listed in the module documentation. It supplies a concrete algebraic check for the Recognition Science claim that macroscopic quantum coherence aligns with the phi fixed point (T6) and the eight-tick octave (T7). No downstream theorems currently depend on it, leaving open whether the same scaling extends to the McMillan exponent or room-temperature theoretical maximum.

scope and limits

formal statement (Lean)

 108theorem cuprate_conventional_ratio :
 109    tcFamily .cuprate / tcFamily .conventional = Constants.phi ^ 3 := by

proof body

Term-mode proof.

 110  dsimp [tcFamily, tc_phonon, familyLadderStep]
 111  -- (1/φ)^3 / (1/φ)^6 = φ^6/φ^3 = φ^3
 112  have hφpos : 0 < Constants.phi := Constants.phi_pos
 113  have hφne : Constants.phi ≠ 0 := ne_of_gt hφpos
 114  have h3 : Constants.phi ^ 3 ≠ 0 := pow_ne_zero 3 hφne
 115  have h6 : Constants.phi ^ 6 ≠ 0 := pow_ne_zero 6 hφne
 116  field_simp
 117
 118/-- The BCS weak-coupling ratio Δ/Tc ≈ 1.76 is related to φ. -/

depends on (8)

Lean names referenced from this declaration's body.