coherent_source_positive
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute the numerical magnitude of the source.
- Does not treat incoherent or partially coherent ensembles.
- Does not incorporate relativistic corrections or quantum fluctuations.
- Does not depend on specific values of the amplitude beyond strict positivity.
formal statement (Lean)
67theorem coherent_source_positive (ens : Ensemble) :
68 0 < coherent_effective_source ens := by
proof body
Term-mode proof.
69 unfold coherent_effective_source
70 exact mul_pos (Nat.cast_pos.mpr ens.N_pos) ens.amplitude_pos
71
72/-! ## 4. Coherence Gain: √N Enhancement -/
73
74/-- The coherence gain: ratio of coherent to incoherent effective source.
75 This equals √N — the enhancement from phase coherence. -/