bcs_ratio_approx
plain-language theorem explainer
The theorem proves that the Recognition Science approximation to the BCS ratio, defined as 2 log φ + 1, lies strictly between 1.7 and 2.1. Researchers modeling superconducting Tc via the φ-gap ladder would cite this interval when checking the golden-ratio proxy against weak-coupling predictions. The proof substitutes the definition, invokes the established bounds 0.48 < log φ < 0.483, and discharges both sides of the conjunction by linear arithmetic.
Claim. Let φ denote the golden ratio. The φ-derived BCS ratio approximation satisfies $1.7 < 2 log φ + 1 < 2.1$.
background
The Superconducting Tc module derives critical temperatures for superconductor families from a φ-gap ladder proxy. Energy gaps Δ scale with φ, Tc follows proportionally under the BCS relation, and macroscopic coherence requires alignment with the eight-tick ledger. The definition bcsDeltaTcRatio computes 2 log φ + 1, presented as an approximation to the experimental weak-coupling value π/e^γ ≈ 1.764. Upstream lemmas supply the tight interval 0.48 < log φ < 0.483 together with the identification of Constants.phi with the golden ratio.
proof idea
The term proof first dsimps the definition of bcsDeltaTcRatio. It rewrites Constants.phi to Real.goldenRatio, then applies the two lemmas log_phi_gt_048 and log_phi_lt_0483 to obtain the bounds on log φ. The constructor splits the conjunction; each inequality is discharged by linarith after observing that 0.48 > 0.35 and 0.483 < 0.55.
why it matters
The result supplies a numerical check for the BCS Relation step inside the CM-007 derivation of Tc families. It relies on the φ fixed point from the forcing chain and the log bounds generated by the numerics interval library. No downstream theorems yet consume the bound, but it closes the claim that the φ-derived value sits in the right ballpark relative to the conventional BCS ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.