CQAligned
The alignment predicate holds for a real threshold θ and CQ value c precisely when θ lies in the closed unit interval and the numerical score of c is at least θ. Researchers working on ethical cost models within Recognition Science cite this predicate when checking admissibility of plans under gap-derived constraints. The definition is introduced as a direct conjunction of the three inequalities with no lemmas or reduction steps required.
claimThe predicate holds for real θ and CQ value c if and only if $0 ≤ θ ≤ 1$ and score(c) ≥ θ, where score extracts the real-valued alignment measure associated to c.
background
In the Ethics.CostModel module, CQ is the alignment type imported from Measurement, and score is the abbrev that maps each CQ instance to its real value. The predicate sits inside the ethical layer that references the 45-gap, whose derivation defines the gap as the product of closure and Fibonacci factors. Upstream results include the period function returning phi raised to an integer power and the gap derivation that fixes the numerical value at 45.
proof idea
The definition is introduced directly as the conjunction of the lower bound on θ, the upper bound on θ, and the comparison of score c to θ; no lemmas are applied and the body contains only the three inequalities.
why it matters in Recognition Science
This definition supplies the alignment check used by the prefer_by_cq theorem, which establishes that higher CQ alignment is preferred in costless ties. It contributes to the ethical extension of the Recognition framework by providing a threshold filter compatible with the 45-gap structure. The predicate therefore links the Measurement-derived CQ scores to the admissibility conditions required by the cost model.
scope and limits
- Does not define the internal structure or constructors of CQ values.
- Does not compute or derive any concrete score values.
- Does not encode the experience requirement tied to the 45-gap period condition.
formal statement (Lean)
68def CQAligned (θ : ℝ) (c : CQ) : Prop :=
proof body
Definition body.
69 0 ≤ θ ∧ θ ≤ 1 ∧ score c ≥ θ
70
71/-- Ethical admissibility under 45‑gap: either no experience required, or the plan includes experience. -/
72/- Placeholder removed: use Gap45 gating rule (experience required iff 8 ∤ period). -/