optimal_iff
plain-language theorem explainer
Quality-equivalent display channels share identical optimal states for any input. Workers on order preservation within the RRF framework cite the result when moving optimality conclusions between observation projections. The proof is a compact term-mode construction that applies the bidirectional quality ordering directly to the two minimality assumptions.
Claim. Let $C_1$ and $C_2$ be display channels over a common state space. If $C_1$ and $C_2$ induce the same ordering on states via their composed quality functions, then a state $x$ achieves the global minimum quality under $C_1$ if and only if it achieves the global minimum quality under $C_2$.
background
A display channel maps each state to an observation and then to a real-valued quality score; the composed stateQuality function therefore ranks states by a single real number. QualityEquiv asserts that two channels produce identical orderings: for every pair of states the inequality between their quality scores holds in one channel exactly when it holds in the other. isOptimal for a channel and a state simply means that the state's quality is less than or equal to the quality of every other state.
proof idea
The term proof builds the biconditional by supplying one function for each direction. The forward direction feeds the optimality hypothesis into the left-to-right half of the QualityEquiv predicate at the given state and arbitrary comparison state. The reverse direction applies the right-to-left half symmetrically.
why it matters
The result is the direct source for the optimal_transfer theorem in the OrderPreservation module, which re-exports the same equivalence for use in larger preservation arguments. It guarantees that optimality is invariant under quality-equivalent re-encodings of the observation space, a prerequisite for consistent multi-channel reasoning inside the RRF core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.