Superconductor
plain-language theorem explainer
The Superconductor structure models an ensemble of Cooper pairs with temperature T and critical temperature Tc > 0, declaring coherence precisely when T < Tc. Researchers modeling coherence-enhanced gravitational sources or the RS antigravity coherence gate would cite this when linking phase transitions to effective source scaling. The declaration is a direct structure with embedded predicates that compare temperature against Tc.
Claim. A superconductor is a structure consisting of an ensemble of $N$ Cooper pairs each of amplitude $a > 0$, a temperature $T$, and critical temperature $T_c > 0$. Coherence holds when $T < T_c$; incoherence holds when $T_c ≤ T$.
background
In the Gravity.CoherenceGain module an Ensemble is a collection of $N$ particles each contributing a vector source of magnitude $a > 0$, with total effective source $N a$ when phases align and $√N a$ when phases are random. The Superconductor structure augments this ensemble by temperature and critical-temperature fields together with the positivity constraint $T_c > 0$. Upstream results supply the eight-tick phase values $kπ/4$ for discrete phase steps and LedgerFactorization for J-cost calibration of sources.
proof idea
Definition of the Superconductor structure together with the two predicates is_coherent and is_incoherent. Each predicate is a direct comparison of the temperature field against the critical_temperature field.
why it matters
This definition supplies the concrete model for the coherence gate: cooling below Tc switches the effective gravitational source from √N a to N a. It is used directly by CoherenceGainCert, coherence_gate, and superconductor_effective_source, which implement the RS Antigravity Whitepaper claim that coherence enhances source strength by √N. The construction sits inside the eight-tick phase framework and supplies an order-parameter example for phase-transition theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.