Ensemble
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.
claimAn 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 in Recognition Science
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.
scope and limits
- Does not encode individual particle phases or their spatial distribution.
- Does not impose any bound on N beyond positivity.
- Does not compute effective sources or the coherence gain itself.
- Does not reference Recognition Science constants such as phi or the eight-tick octave.
formal statement (Lean)
35structure Ensemble where
36 N : ℕ
37 N_pos : 0 < N
38 individual_amplitude : ℝ
39 amplitude_pos : 0 < individual_amplitude
40
41/-! ## 2. Incoherent Ensemble: Random Walk -/
42
43/-- For an incoherent ensemble (random phases), the effective source magnitude
44 is √N × individual amplitude (random walk / central limit theorem).
45
46 This is because N unit vectors with random phases sum to magnitude ~ √N. -/