coherent_source_positive
plain-language theorem explainer
The declaration establishes that the coherent effective source strength for any ensemble of particles is strictly positive. Modelers of phase-locked gravitational sources in Recognition Science would cite it to guarantee non-vanishing terms under constructive interference. The argument is a direct term-mode reduction that unfolds the source definition and applies the positivity of real multiplication to the cast particle count and individual amplitude.
Claim. Let $E$ be an ensemble of $N>0$ particles each with positive amplitude $a$. Then the coherent effective source $S_c(E)$ satisfies $S_c(E)>0$.
background
In the CoherenceGain module an Ensemble is a structure consisting of a positive natural number $N$ of particles together with a positive real individual amplitude $a$. The coherent effective source is defined as the product $N a$, which encodes perfect phase alignment across the ensemble. This construction sits inside the Recognition Science treatment of gravity, where source magnitudes are derived from ledger factorization and spectral emergence imported from upstream modules.
proof idea
The proof is a one-line term that unfolds the definition of the coherent effective source and applies the mul_pos lemma to the positivity of the cast natural number $N$ and the individual amplitude.
why it matters
This result secures the positivity hypothesis required for the subsequent coherence-gain calculations in the same module, including the square-root-$N$ enhancement formula. It draws on the eight-tick phase definition to ensure that coherent summation over the discrete phases yields a non-vanishing contribution, consistent with the T7 octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.