cooper_pair_binding_exceeds_thermal
plain-language theorem explainer
The theorem establishes that the critical temperature T_c(n) on the phi-ladder satisfies T_c(n) ≥ 1 for every integer n ≥ 0. Materials scientists checking room-temperature superconductivity conditions would cite this structural bound when verifying that phi-coherent pairing overcomes thermal fluctuations. The proof reduces to unfolding T_c_rung as phi to the power n, splitting on whether n equals zero or is positive, and invoking the fact that phi exceeds one.
Claim. For every integer $n ≥ 0$, the critical temperature $T_c(n) = φ^n$ on the phi-ladder satisfies $1 ≤ T_c(n)$, where $φ$ denotes the golden ratio.
background
The module derives room-temperature superconductivity conditions from the phi-ladder energy structure in Recognition Science. T_c_rung(n) is defined as phi^n, representing the critical temperature at rung n in units scaled so the coherence quantum sets the base. The local setting requires Cooper pair binding energy to exceed k_B T, with E_coh = phi^{-5} exceeding room-temperature thermal energy and each material occupying a specific rung n.
proof idea
The proof unfolds the definition of T_c_rung to obtain phi^n. It performs case analysis via rcases on hn.lt_or_eq to separate n = 0 from n > 0. The positive case applies one_lt_zpow₀ one_lt_phi to obtain the inequality; the zero case follows by direct simplification.
why it matters
This result supplies the key inequality for the EN-002 certificate, confirming that binding exceeds thermal energy on non-negative rungs and supporting the module's hierarchy of coherence, temperature, and pressure conditions. It connects directly to the phi-ladder monotonicity and the framework claim that ambient superconductivity is possible under phi-coherent pairing. The declaration closes one structural step in the EN-002 derivation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.