coherence_gate
plain-language theorem explainer
The coherence gate establishes that any superconductor whose Cooper-pair ensemble satisfies N ≥ 2 has a strictly larger effective gravitational source in the coherent state than in the incoherent state. Researchers modeling the RS antigravity proposal cite the gate when they switch source strength across Tc. The proof is a one-line term wrapper that unfolds the superconductor source definition and applies the coherent-exceeds-incoherent comparison.
Claim. Let $sc$ be a superconductor whose Cooper-pair ensemble has size $N ≥ 2$. Then the incoherent effective source is strictly smaller than the coherent effective source: $√N · a < N · a$, where $a$ is the amplitude of a single Cooper pair.
background
The CoherenceGain module treats an Ensemble as a finite collection of N identical oscillators, each with amplitude a. The incoherent effective source is defined as √N · a, the magnitude obtained from a random-phase sum. The coherent effective source is N · a. A Superconductor is a structure that pairs such an Ensemble with a temperature and a critical temperature; below Tc the pairs share a common phase and the ensemble is treated as coherent.
proof idea
The proof is a one-line term-mode wrapper. It simplifies superconductor_effective_source sc true to the coherent effective source on the Cooper-pair ensemble, then applies the upstream theorem coherent_exceeds_incoherent together with the supplied bound 2 ≤ N.
why it matters
The theorem supplies the superconductor_gate field of the CoherenceGainCert certificate. It encodes the Coherence Gate described in the RS Antigravity Whitepaper, the step that converts the √N incoherent source into the N coherent source when the material is cooled below Tc. The result is invoked by coherence_gain_certified to certify the overall gain formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.