coherence_gain_certified
plain-language theorem explainer
The coherence gain certified theorem packages three results into a single certificate: coherence gain equals √N for any ensemble, coherent effective sources strictly exceed incoherent ones for N ≥ 2, and superconductors satisfy the coherence gate that enhances effective source strength. Gravitational coherence and antigravity modelers cite it to quantify √N enhancement from phase coherence. The proof is a term-mode structure construction that directly references the three supporting lemmas on gain equality, source comparison, and the supercondo
Claim. Let CoherenceGainCert be the structure asserting that for every ensemble E the coherence gain equals √N, that the incoherent effective source is strictly less than the coherent effective source whenever N ≥ 2, and that for a superconductor with at least two Cooper pairs the incoherent source is less than the superconductor effective source when coherence is enabled.
background
In the Gravity.CoherenceGain module an Ensemble consists of a particle count N together with an individual amplitude that is positive. The coherence gain is the ratio of coherent to incoherent effective sources; the upstream lemma coherence_gain_eq_sqrt_N shows this ratio simplifies exactly to √N by algebraic cancellation of the amplitude terms. The incoherent effective source is defined as (N · amplitude) / (√N · amplitude) while the coherent version is N · amplitude. A Superconductor is an ensemble of Cooper pairs equipped with a coherence flag that selects the effective source via an if-then-else. The local setting is the Recognition Science treatment of gravity as a coherence phenomenon, with the coherence gate realizing the enhancement described in the RS Antigravity Whitepaper.
proof idea
The proof is a term-mode construction of the CoherenceGainCert structure. It supplies the gain_is_sqrt_N field by direct reference to coherence_gain_eq_sqrt_N, the coherent_beats_incoherent field by coherent_exceeds_incoherent, and the superconductor_gate field by the lambda abstraction fun sc hN => coherence_gate sc hN.
why it matters
This theorem supplies the gap3_coherence_gain component required by the levitation certificates forcing_chain_complete, full_levitation_cert and levitation_unconditional in the AcousticPhaseLevitation module. It realizes the Coherence Gate from the RS Antigravity Whitepaper and the √N scaling that appears in the forcing chain T0–T8. The result is fully proved and closes the coherence-gain scaffolding step with no remaining open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.