CQ
plain-language theorem explainer
CQ is the coherence quotient alias re-exported into the ethics cost model from the Measurement module, consisting of listensPerSec, opsPerSec, and coherence8 bounded in [0,1]. Researchers building ethical preference relations under Recognition Science would cite this to keep the alignment descriptor uniform across layers. The declaration is a direct one-line abbreviation with no proof obligations.
Claim. Let $CQ$ denote the coherence quotient structure with fields listensPerSec, opsPerSec, and coherence8 satisfying $0 ≤$ coherence8 $≤ 1$.
background
The Ethics.CostModel module defines preference and admissibility relations that depend on a coherence measure. CQ is the imported descriptor from Measurement whose coherence8 field carries explicit bounds. Upstream Measurement.CQ witnesses 0 ≤ coherence8 ≤ 1 while Data.Import.Measurement supplies a generic name-value-error triple and RSNative.Core.Measurement adds protocol and uncertainty fields.
proof idea
This is a one-line abbreviation that directly imports the CQ structure from IndisputableMonolith.Measurement.CQ.
why it matters
The alias feeds Admissible, CQAligned, PreferLex, prefer_by_cq, and score inside the same module, which in turn support ethical admissibility under the 45-gap rule from Gap45.Beat. It supplies the coherence threshold θ ∈ [0,1] used in alignment checks that appear in the prefer_by_cq theorem. The declaration closes a placeholder noted in the module doc-comment and connects to the Recognition framework's coherence measures without yet linking to the phi-ladder or J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.