structure definition def or abbrev

`CQ`

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

formal statement (Lean)

  80structure CQ where
  81  listensPerSec : ℝ
  82  opsPerSec : ℝ
  83  coherence8 : ℝ
  84  coherence8_bounds :
  85    0 ≤ coherence8 ∧ 0 ≤ coherence8 ∧ coherence8 ≤ 1 ∧ coherence8 ≤ 1
  86
  87/-- CQ score; zero when the operations-per-second denominator vanishes. -/

used by (11)

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

Admissible in IndisputableMonolith.Ethics.CostModel decl_use
CQ in IndisputableMonolith.Ethics.CostModel decl_use
CQAligned in IndisputableMonolith.Ethics.CostModel decl_use
improves_comp_left in IndisputableMonolith.Ethics.CostModel decl_use
prefer_by_cq in IndisputableMonolith.Ethics.CostModel decl_use
PreferLex in IndisputableMonolith.Ethics.CostModel decl_use
requiresExperience in IndisputableMonolith.Ethics.CostModel decl_use
score in IndisputableMonolith.Ethics.CostModel decl_use
requiresExperience in IndisputableMonolith.Gap45.Beat decl_use
avg in IndisputableMonolith.Measurement decl_use
score in IndisputableMonolith.Measurement decl_use

depends on (3)

Lean names referenced from this declaration's body.

CQ in IndisputableMonolith.Ethics.CostModel decl_use
score in IndisputableMonolith.Ethics.CostModel decl_use
score in IndisputableMonolith.Measurement decl_use