superconducting_gap
The superconducting gap function in Recognition Science is defined as E_coh times (1 - T/T_c) when T is below the critical temperature T_c and zero otherwise. Researchers deriving room-temperature superconductivity conditions from the φ-ladder would cite this when analyzing gap temperature dependence. The definition is a direct piecewise expression built from the coherence quantum E_coh = φ^{-5}.
claimThe gap function is defined by $Δ(T, T_c) = E_{coh} (1 - T/T_c)$ for $T < T_c$ and $Δ(T, T_c) = 0$ otherwise, where $E_{coh} = φ^{-5}$ is the RS coherence quantum and $T_c > 0$.
background
The EN-002 module derives room-temperature superconductivity from the φ-ladder energy structure. Superconductivity requires Cooper pair formation with binding energy at least k_B T; in RS the pairing scale is quantized as E_n = E_coh · φ^n with E_coh = φ^{-5} ≈ 0.090 eV. This exceeds room-temperature thermal energy (≈ 0.026 eV), so φ-coherent materials can superconduct at ambient conditions. The module lists supporting results including rs_coherence_quantum_pos (E_coh > 0) and phi_ladder_tc_monotone (higher rung yields higher T_c).
proof idea
This is a direct definition via if-then-else on the comparison T < T_c. It inserts the sibling E_coh definition and the linear thermal suppression factor (1 - T/T_c).
why it matters in Recognition Science
The definition supplies the explicit gap expression used by gap_max_at_zero, gap_zero_above_tc, superconducting_gap_positive and the central room_temperature_superconductivity_from_ledger theorem. It realizes the EN-002.7 slot in the hierarchy of conditions, linking the coherence quantum E_coh = φ^{-5} to the observable gap that vanishes above T_c. The construction sits inside the Recognition Science forcing chain by tying the T5 J-uniqueness and T6 φ fixed-point to an engineering-scale prediction for ambient superconductivity.
scope and limits
- Does not derive T_c from microscopic material parameters.
- Does not include pressure or rung-selection effects on the φ-ladder.
- Does not specify the lattice conditions needed for φ-coherence.
- Does not convert the gap to SI units or predict numerical values for specific compounds.
formal statement (Lean)
110def superconducting_gap (T : ℝ) (T_c : ℝ) (hTc : 0 < T_c) : ℝ :=
proof body
Definition body.
111 if T < T_c then E_coh * (1 - T / T_c) else 0
112
113/-- **THEOREM EN-002.7**: The superconducting gap is positive when T < T_c. -/