score
plain-language theorem explainer
The score abbrev maps a coherence quotient CQ to a real number via the ratio of listens-per-second to operations-per-second scaled by the coherence8 factor, returning zero when the denominator vanishes. Researchers modeling ethics costs or applying coherence metrics in visual aesthetics and exoplanet habitability would cite this definition. The implementation is a direct one-line alias to the core Measurement.score function.
Claim. Let $c$ be a coherence quotient with fields listensPerSec, opsPerSec, and coherence8. Then score$(c) = 0$ if opsPerSec$(c) = 0$, otherwise $(listensPerSec(c) / opsPerSec(c)) * coherence8(c)$.
background
In the Ethics.CostModel module, CQ is an alias to the Measurement.CQ structure consisting of three real components: listensPerSec, opsPerSec, and coherence8, with explicit bounds $0 ≤ coherence8 ≤ 1$. The score originates from the Measurement module definition that normalizes the listen-to-operation ratio by the coherence factor while guarding against division by zero. The module imports Mathlib and Gap45.Beat but delegates its type and computation to the Measurement and Data.Import layers.
proof idea
This is a one-line wrapper that applies the IndisputableMonolith.Measurement.score definition to the input CQ.
why it matters
This definition supplies the coherence metric referenced by downstream results including beautyScore and visualBeautyCert in Aesthetics.VisualBeauty plus habitability_score in Astrophysics.ExoplanetHabitability. It supplies the uniform score inside the ethics cost model, linking concrete measurement structures to applications that compare recognition costs via J-cost and phi-ladder relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.