coherent_exceeds_incoherent
plain-language theorem explainer
For an ensemble of N particles with N at least 2, the coherent effective source magnitude strictly exceeds the incoherent random-walk magnitude. Gravity and superconductivity models cite this to certify coherence gain. The tactic proof unfolds the two source definitions, records positivity of N and sqrt(N), proves sqrt(N) < N by squaring and comparison to sqrt(2), then closes with nlinarith.
Claim. Let $a > 0$ be the individual amplitude of an ensemble of $N$ particles with $N$ a natural number satisfying $N ≥ 2$. Then the incoherent effective source magnitude $√N · a$ is strictly less than the coherent effective source magnitude $N · a$.
background
An Ensemble is a structure consisting of a natural number N > 0 together with a positive real individual amplitude a. The incoherent effective source is the random-walk magnitude √N · a. The coherent effective source is the phase-aligned sum N · a. This declaration lives in the Gravity.CoherenceGain module, which treats coherence enhancement for gravitational sources and superconducting Cooper-pair ensembles. It draws on the eight-tick phase definition and the active-edge count A from the foundation layer.
proof idea
The proof unfolds incoherent_effective_source and coherent_effective_source. It obtains positivity of N and of √N from Nat.cast_pos and Real.sqrt_pos. It shows √N < N by squaring, using Real.mul_self_sqrt and a comparison of √2 to √N. The final step applies nlinarith to the resulting strict inequality.
why it matters
coherent_exceeds_incoherent is invoked directly by coherence_gain_certified to certify the gain property and by coherence_gate to realize the coherence gate for superconductors below Tc. It supplies the strict inequality required by the RS Antigravity Whitepaper for the coherence-gate mechanism. The result sits inside the T7 eight-tick octave and supports the D = 3 spatial-dimension forcing step by enabling phase-coherent source summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.