incoherent_source_positive
plain-language theorem explainer
The theorem proves that the incoherent effective source of any ensemble is strictly positive. Researchers modeling random-phase sources in gravitational coherence or ledger calculations would cite it to guarantee non-vanishing contributions from incoherent ensembles. The term proof unfolds the source definition and applies multiplication positivity to the square-root factor and the amplitude.
Claim. Let $ens$ be an ensemble with $N>0$ particles each of positive amplitude $a$. Then the incoherent effective source equals $a$ times the square root of $N$ and is therefore positive.
background
In the Gravity.CoherenceGain module an Ensemble is the structure carrying a positive natural number $N$ of particles together with a positive real individual amplitude $a$. For incoherent ensembles the effective source is defined by random-walk summation, yielding the product of $a$ and the square root of $N$. This positivity statement belongs to the local contrast between incoherent and coherent summation that the module uses to derive effective gravitational strengths from Recognition Science ledger rules.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of incoherent_effective_source, then applies mul_pos. The first factor is shown positive by composing Nat.cast_pos with Real.sqrt_pos; the second factor is supplied directly by the ensemble field amplitude_pos.
why it matters
The result supplies the base positivity required for the coherence_gain and coherent_exceeds_incoherent calculations that follow in the same module. It thereby anchors the incoherent half of the ensemble comparison used in gravity coherence arguments. No open scaffolding remains; the claim is fully discharged inside the Recognition Science treatment of phase-dependent source magnitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.