ratio_approx_3_52
plain-language theorem explainer
The theorem verifies that 3.52 is strictly less than 4/1.134, which evaluates to approximately 3.528 and matches the BCS gap ratio 2Δ/k_B T_c. Physicists deriving superconductivity from J-cost minimization cite it to confirm numerical consistency of the universal ratio. The proof is a direct real-number evaluation.
Claim. $3.52 < 4/1.134$, confirming the BCS universal ratio $2Δ/(k_B T_c) ≈ 3.52$.
background
The CooperPair module derives BCS superconductivity from J-cost submultiplicativity: time-reversed electron pairs reach J(x · x^{-1}) = 0. The module states that pairing is energetically favored and produces the universal ratio 2Δ/(k_B T_c) ≈ 3.52. Upstream, RSNativeUnits.U fixes c = 1 and τ₀ = 1 tick while EightTick.phase supplies the 8-tick phases kπ/4 that calibrate the ledger.
proof idea
One-line wrapper that applies norm_num to evaluate the real inequality directly.
why it matters
It anchors the bcs_gap_ratio claim inside the same module, which traces back to T5 J-uniqueness and T7 eight-tick octave in the forcing chain. The numerical check closes the loop between abstract J-cost minimization and the observed BCS value of 3.52.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.