abbrev definition def or abbrev

`CQ`

show as: view Lean formalization →

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

generate prose now

formal statement (Lean)

  66abbrev CQ := IndisputableMonolith.Measurement.CQ

used by (11)

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

Admissible 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
CQ in IndisputableMonolith.Measurement decl_use
score in IndisputableMonolith.Measurement decl_use

depends on (4)

Lean names referenced from this declaration's body.

Measurement in IndisputableMonolith.Data.Import decl_use
CQ in IndisputableMonolith.Measurement decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use