CoherenceGainCert
plain-language theorem explainer
CoherenceGainCert bundles the equality of coherence gain to sqrt(N) for any ensemble, the strict inequality of coherent over incoherent effective sources for N at least 2, and the superconductor gate condition. Researchers modeling RS antigravity via phase coherence cite it to certify the enhancement of gravitational sources below T_c. The declaration is a direct structure definition that collects three properties already proved by sibling lemmas on effective sources.
Claim. A structure asserting that for any ensemble $E$ the coherence gain equals $N^{1/2}$, that the incoherent effective source is strictly less than the coherent effective source whenever $Ngeq 2$, and that for a superconductor $S$ with at least two Cooper pairs the incoherent source of its pairs is strictly less than the coherent effective source of $S$.
background
In Gravity.CoherenceGain an Ensemble is a finite collection of $N$ particles each carrying an individual amplitude $a>0$; the total gravitational source magnitude depends on whether the phases are aligned. Coherent effective source sums the amplitudes linearly to $N a$, while incoherent effective source follows the random-walk scaling $sqrt(N) a$. A Superconductor is an Ensemble of Cooper pairs together with a temperature and critical temperature $T_c>0$; below $T_c$ the pairs form a single macroscopic phase-coherent state.
proof idea
CoherenceGainCert is a structure definition with an empty proof body. It directly records three fields: the equality supplied by coherence_gain_eq_sqrt_N, the inequality supplied by coherent_exceeds_incoherent, and the gate supplied by coherence_gate. No tactics or reductions are performed; the declaration simply packages the three properties.
why it matters
The structure supplies the certified interface for the Coherence Gate in Recognition Science gravity models. It is instantiated by coherence_gain_certified and consumed by UnconditionalLevitationCert as one of the bridge certificates leading to acoustic phase levitation. The declaration realizes the statement from the RS Antigravity Whitepaper that cooling below $T_c$ multiplies the effective source by $sqrt(N)$, consistent with the framework's treatment of phase coherence as a source of macroscopic gravitational enhancement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.