def definition def or abbrev

`coherent_effective_source`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  64def coherent_effective_source (ens : Ensemble) : ℝ :=

Definition body.

  65  ens.N * ens.individual_amplitude
  66

From the project-wide theorem graph. These declarations reference this one in their body.

coherence_gain in IndisputableMonolith.Gravity.CoherenceGain decl_use
CoherenceGainCert in IndisputableMonolith.Gravity.CoherenceGain decl_use
coherence_gain_eq_sqrt_N in IndisputableMonolith.Gravity.CoherenceGain decl_use
coherent_exceeds_incoherent in IndisputableMonolith.Gravity.CoherenceGain decl_use
coherent_source_positive in IndisputableMonolith.Gravity.CoherenceGain decl_use
superconductor_effective_source in IndisputableMonolith.Gravity.CoherenceGain decl_use

Lean names referenced from this declaration's body.