CQAligned
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.