gap_max_at_zero
plain-language theorem explainer
The superconducting gap function attains its maximum value of the coherence quantum E_coh exactly at zero temperature for any positive critical temperature. Materials scientists bounding pairing energies in room-temperature superconductivity derivations would cite this result. The proof is a direct term-mode unfolding of the gap definition followed by simplification under the positivity hypothesis on T_c.
Claim. For any $T_c > 0$, the superconducting gap satisfies $Δ(0, T_c) = E_{coh}$, where $E_{coh} = φ^{-5}$ is the RS coherence quantum and $Δ(T, T_c) = E_{coh}(1 - T/T_c)$ whenever $T < T_c$.
background
The module derives ambient superconductivity conditions from the φ-ladder energy structure, with pairing energy quantized as $E_n = E_{coh} · φ^n$. The coherence quantum is defined as $E_{coh} := φ^{-5}$, which equals approximately 0.090 eV and exceeds room-temperature thermal energy. The gap function itself is the piecewise definition that returns $E_{coh}(1 - T/T_c)$ below $T_c$ and zero above it, as stated in the upstream superconducting_gap declaration.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of superconducting_gap and applies simp using the hypothesis that $T_c > 0$, which selects the superconducting branch and reduces the expression at $T = 0$ directly to $E_{coh}$.
why it matters
Labeled EN-002.9, this theorem supplies the zero-temperature bound required by the en002_certificate that certifies the full room-temperature superconductivity derivation. It confirms the expected maximum of the gap function within the φ-ladder framework (T5 J-uniqueness and T6 self-similar fixed point) and supports the claim that coherent pairing exceeds thermal fluctuations at ambient conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.