superconductor_effective_source
plain-language theorem explainer
The definition selects the effective gravitational source strength of a superconductor by dispatching on a coherence flag. Researchers modeling the coherence gate in gravity would cite it to switch between N-scaling and √N-scaling regimes. Implementation is a direct conditional that routes the Cooper-pair ensemble to either the coherent or incoherent source function.
Claim. Let $sc$ be a superconductor whose Cooper-pair ensemble $E$ has size $N$ and individual amplitude $a$. The effective source equals $N a$ when the coherence flag is true and equals $a$ times the square root of $N$ when the flag is false.
background
In the Gravity.CoherenceGain module a Superconductor is the structure holding an Ensemble of Cooper pairs, a temperature value, and a critical temperature with the positivity constraint $0 <$ critical_temperature. The predicate is_coherent holds precisely when temperature lies below critical_temperature. The upstream coherent_effective_source returns the product of ensemble size and individual amplitude for any phase-aligned ensemble; its incoherent counterpart supplies the square-root scaling.
proof idea
One-line wrapper that applies coherent_effective_source to the cooper_pairs field when the Boolean flag is true and otherwise applies incoherent_effective_source to the same field.
why it matters
The definition supplies the state selector required by the coherence_gate theorem and the CoherenceGainCert structure. It encodes the coherence gate of the RS Antigravity Whitepaper, switching the ledger from √N to N scaling once the superconductor drops below T_c. The construction sits inside the Recognition Science treatment of coherence-enhanced gravitational sources.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.