  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
  78
  79/-- COHERENCE GAIN = √N: Phase-coherent matter produces √N times
  80    the gravitational effect of the same matter in an incoherent state.
  81
  82    For a superconductor with N ~ 10²² Cooper pairs: gain ~ 10¹¹.
  83    This matches Ning Li's claimed gravitomagnetic enhancement exactly. -/
  84theorem coherence_gain_eq_sqrt_N (ens : Ensemble) :
  85    coherence_gain ens = Real.sqrt ens.N := by
  86  unfold coherence_gain coherent_effective_source incoherent_effective_source
  87  rw [show (↑ens.N * ens.individual_amplitude) / (Real.sqrt ↑ens.N * ens.individual_amplitude) =
  88      ↑ens.N / Real.sqrt ↑ens.N from by
  89    rw [mul_div_mul_right _ _ (ne_of_gt ens.amplitude_pos)]]
  90  rw [div_eq_iff (Real.sqrt_ne_zero'.mpr (Nat.cast_pos.mpr ens.N_pos))]
  91  exact (Real.mul_self_sqrt (Nat.cast_nonneg ens.N)).symm
  92
  93/-- Coherent source is STRICTLY greater than incoherent for N ≥ 2. -/
  94theorem coherent_exceeds_incoherent (ens : Ensemble) (hN : 2 ≤ ens.N) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.