incoherent_effective_source

formal source

  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
  66
  67theorem coherent_source_positive (ens : Ensemble) :
  68    0 < coherent_effective_source ens := by
  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. -/
  76def coherence_gain (ens : Ensemble) : ℝ :=
  77  coherent_effective_source ens / incoherent_effective_source ens