Ensemble

formal source

  32
  33/-- An ensemble of N particles, each contributing a vector source of magnitude `a`.
  34    The total effective source depends on phase coherence. -/
  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. -/
  47def incoherent_effective_source (ens : Ensemble) : ℝ :=
  48  Real.sqrt ens.N * ens.individual_amplitude
  49
  50theorem incoherent_source_positive (ens : Ensemble) :
  51    0 < incoherent_effective_source ens := by
  52  unfold incoherent_effective_source
  53  apply mul_pos
  54  · exact Real.sqrt_pos.mpr (Nat.cast_pos.mpr ens.N_pos)
  55  · exact ens.amplitude_pos
  56
  57/-! ## 3. Coherent Ensemble: Constructive Summation -/
  58
  59/-- For a coherent ensemble (all phases aligned, e.g., BEC/superconductor),
  60    the effective source magnitude is N × individual amplitude.
  61
  62    All N vectors point in the same direction → linear sum.
  63    The ledger sees one macro-object of multiplicity N. -/
  64def coherent_effective_source (ens : Ensemble) : ℝ :=
  65  ens.N * ens.individual_amplitude