coherent_effective_source
plain-language theorem explainer
The definition assigns to each ensemble of N aligned particles the effective gravitational source strength N times the individual amplitude. Researchers modeling gravitational signatures of Bose-Einstein condensates or superconductors cite this quantity when computing coherence-enhanced effects. It is a direct one-line multiplication that follows from vector addition under perfect phase alignment.
Claim. For an ensemble $ens$ consisting of $N$ particles each of amplitude $a>0$, the coherent effective source magnitude is $N a$.
background
In the Gravity.CoherenceGain module an Ensemble is a structure that records the particle count $N$ together with proofs that $N>0$ and that the individual amplitude $a>0$. The coherent case assumes all phases are aligned, so the vector sources add linearly rather than executing a random walk. This definition supplies the numerator for the coherence-gain ratio that downstream results equate to $√N$. The module imports only Mathlib and rests directly on the Ensemble structure.
proof idea
One-line definition that multiplies the ensemble cardinality by the individual amplitude.
why it matters
This definition is the building block for the coherence-gain theorem, which states that phase-coherent matter produces $√N$ times the gravitational effect of the same matter in an incoherent state. It feeds the CoherenceGainCert structure and the superconductor effective source definition, realizing the coherence gate from the RS Antigravity Whitepaper. For $N$ around $10^{22}$ Cooper pairs the gain reaches $10^{11}$, matching claimed gravitomagnetic enhancements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.