trans
Quality equivalence of display channels is transitive. Researchers working with chained observation projections in RRF models would cite this result when composing channels. The proof is a one-line term that chains the two biconditionals via transitivity of logical equivalence on the induced state orderings.
claimLet $C_1$, $C_2$, $C_3$ be display channels sharing a common state space. If $C_1$ and $C_2$ induce identical orderings on states via their composed quality functions and $C_2$ and $C_3$ induce identical orderings, then $C_1$ and $C_3$ induce identical orderings.
background
A display channel consists of an observation map from states to an observation space together with a real-valued quality function on observations. The composed state quality is obtained by applying the quality function after the observation map. Quality equivalence is the relation that holds precisely when two channels produce the same preorder on states under this composed quality measure.
proof idea
The proof is a one-line term that applies transitivity of the biconditional: for arbitrary states x and y the ordering equivalence supplied by the first hypothesis is chained with the ordering equivalence supplied by the second hypothesis.
why it matters in Recognition Science
The result completes the demonstration that quality equivalence is an equivalence relation on display channels, supporting downstream statements about optimal states and global optimality by permitting channel composition without altering the induced ranking. It sits inside the RRF core module whose purpose is to furnish consistent observation projections for the Recognition framework.
scope and limits
- Does not define the concrete computation of the composed quality function.
- Does not impose any relation between the distinct observation spaces.
- Does not extend the relation to strict inequalities or other order properties.
- Does not address continuity, measurability, or computational cost of the channels.
formal statement (Lean)
65theorem trans {C₁ : DisplayChannel State Obs₁}
66 {C₂ : DisplayChannel State Obs₂}
67 {C₃ : DisplayChannel State Obs₃}
68 (h₁₂ : QualityEquiv C₁ C₂) (h₂₃ : QualityEquiv C₂ C₃) : QualityEquiv C₁ C₃ :=
proof body
Term-mode proof.
69 fun x y => (h₁₂ x y).trans (h₂₃ x y)
70
71/-- Quality-equivalent channels have the same optimal states. -/