def definition def or abbrev

`score`

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

formal statement (Lean)

  88@[simp] noncomputable def score (c : CQ) : ℝ :=

Definition body.

  89  if c.opsPerSec = 0 then 0 else (c.listensPerSec / c.opsPerSec) * c.coherence8
  90
  91end Measurement
  92end IndisputableMonolith

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

beautyScore in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
beautyScore_at_one in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
ruleOfThirds_lattice_period_eq in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
visualBeautyCert in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
habitability_score in IndisputableMonolith.Astrophysics.ExoplanetHabitability decl_use
T_RS_period_pos in IndisputableMonolith.Astrophysics.ExoplanetHabitability decl_use
PublicInvariant in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
CQAligned in IndisputableMonolith.Ethics.CostModel decl_use
improves_comp_left in IndisputableMonolith.Ethics.CostModel decl_use
score in IndisputableMonolith.Ethics.CostModel decl_use
eightGateNeutral in IndisputableMonolith.Flight.Schedule decl_use
neutralityScore in IndisputableMonolith.Flight.Schedule decl_use
CQ in IndisputableMonolith.Measurement decl_use
eightGateNeutral in IndisputableMonolith.Spiral.SpiralField decl_use

Lean names referenced from this declaration's body.