abbrev 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)

  67@[simp] abbrev score (c : CQ) : ℝ := IndisputableMonolith.Measurement.score c

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
eightGateNeutral in IndisputableMonolith.Flight.Schedule decl_use
neutralityScore in IndisputableMonolith.Flight.Schedule decl_use
CQ in IndisputableMonolith.Measurement decl_use
score in IndisputableMonolith.Measurement decl_use
eightGateNeutral in IndisputableMonolith.Spiral.SpiralField decl_use

Lean names referenced from this declaration's body.