Ensemble
plain-language theorem explainer
Ensemble is a structure for N particles each emitting amplitude a, used to separate coherent linear summation from incoherent random-walk summation in gravitational source calculations. Gravity modelers cite it when deriving the sqrt(N) coherence gain for superconductors and Bose condensates. The declaration is a bare structure definition with four fields enforcing positivity.
Claim. An ensemble consists of a positive integer $N$ and a positive real number $a$, where $N$ counts the particles and $a$ is the amplitude of each particle's vector source.
background
In Gravity.CoherenceGain the Ensemble structure supplies the parameters for effective-source definitions. Upstream amplitude notions appear in QFT.SMatrixUnitarity (S-matrix element between states) and Quantum.DoubleSlit (sum of two complex path phases). The positivity constraints N > 0 and a > 0 ensure that both coherent and incoherent source magnitudes remain strictly positive, as required by the downstream theorems coherent_source_positive and incoherent_source_positive.
proof idea
This is a structure definition with no proof body or applied lemmas.
why it matters
Ensemble supplies the input type for coherence_gain, coherence_gain_eq_sqrt_N, and CoherenceGainCert. The latter records the coherence gate: cooling below Tc makes incoherent source strictly smaller than the coherent source for N >= 2. This supplies the mathematical step behind the RS claim that phase-coherent matter yields sqrt(N) gravitational enhancement, matching the Ning Li gravitomagnetic factor for N ~ 10^22 Cooper pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.