QualityEquiv
QualityEquiv declares two display channels equivalent precisely when their stateQuality maps induce identical orderings on the shared state space. Workers on order preservation and channel interchange in recognition models cite it to equate observation projections without altering optimality conclusions. The declaration is a direct biconditional abbreviation on pairwise quality comparisons.
claimTwo display channels $C_1$ and $C_2$ are quality-equivalent if for all states $x,y$ one has $C_1.stateQuality(x) ≤ C_1.stateQuality(y) ↔ C_2.stateQuality(x) ≤ C_2.stateQuality(y)$.
background
A display channel is a structure carrying an observation map State → Obs together with a real-valued quality function Obs → ℝ. The stateQuality operation composes these maps to produce a direct real-valued quality on states. The module presents channels as distinct projections or observations of the same underlying state space.
proof idea
As an abbreviation the declaration directly encodes the biconditional on the orderings induced by the two stateQuality functions. No lemmas or tactics are invoked; the definition itself supplies the equivalence predicate used by the surrounding theorems.
why it matters in Recognition Science
QualityEquiv supplies the relation that optimal_iff and optimal_transfer invoke to equate optimal states across channels. It also grounds the equivalence-relation theorems refl, symm and trans, and is re-exported as ChannelEquiv in the glossary. In the Recognition framework it supports consistency conditions by permitting interchangeable observation channels while preserving induced orderings on states.
scope and limits
- Does not construct any observe or quality maps.
- Does not require channels to agree on observation values, only on induced orderings.
- Does not impose continuity or other regularity on the quality functions.
- Does not address multi-channel bundles or global optimality.
formal statement (Lean)
48abbrev QualityEquiv {State Obs₁ Obs₂ : Type*}
49 (C₁ : DisplayChannel State Obs₁)
50 (C₂ : DisplayChannel State Obs₂) : Prop :=
proof body
Definition body.
51 ∀ x y : State, C₁.stateQuality x ≤ C₁.stateQuality y ↔
52 C₂.stateQuality x ≤ C₂.stateQuality y
53
54namespace QualityEquiv
55
56variable {State Obs₁ Obs₂ Obs₃ : Type*}
57