coherence_gain_eq_sqrt_N
plain-language theorem explainer
The theorem establishes that the coherence gain for an ensemble of N particles equals the square root of N. Gravitational physicists modeling phase-coherent sources such as superconductors would cite this identity to quantify the enhancement of effective gravitational strength. The proof is a direct algebraic simplification obtained by unfolding the coherent and incoherent source definitions and cancelling common factors using square-root identities.
Claim. Let $E$ be an ensemble of $N$ particles each of positive amplitude $a$. The coherence gain of $E$, defined as the ratio of its coherent effective source magnitude to its incoherent effective source magnitude, equals $N^{1/2}$.
background
The Ensemble structure collects $N$ particles, each emitting a source vector of fixed magnitude $a > 0$. For incoherent phases the effective source follows random-walk scaling and therefore equals $N^{1/2} a$. For coherent phases the sources add linearly, giving $N a$. The coherence gain is the ratio of these two quantities, which the present theorem shows simplifies exactly to $N^{1/2}$ once the common amplitude is cancelled.
proof idea
The term proof unfolds the definitions of coherence_gain, coherent_effective_source and incoherent_effective_source. It rewrites the ratio $(N a)/(N^{1/2} a)$ by cancelling the common positive amplitude factor, reduces the remaining expression $N/N^{1/2}$ via the identity $N^{1/2} N^{1/2} = N$, and concludes with the symmetric form of the square-root multiplication rule.
why it matters
This identity supplies the central computational step inside coherence_gain_certified, which packages the square-root law together with the strict inequality for $N$ at least 2 and the superconductor gate. Within the Recognition Science framework it supplies the quantitative link between phase coherence and gravitational amplification, reproducing the order-of-magnitude enhancement reported for superconducting samples with $N$ near $10^{22}$. The result closes the purely kinematic part of the coherence-gain argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.