optimal_iff
Quality-equivalent display channels share identical optimal states. Researchers working on invariance properties in recognition fields cite this to transfer optimality across observation projections. The proof is a direct term-mode biconditional that applies the forward and reverse directions of the quality-ordering equivalence to the two minimality predicates.
claimLet $C_1$ and $C_2$ be display channels on a common state space. If $C_1$ and $C_2$ are quality-equivalent (i.e., they induce identical orderings on states via their composed quality functions), then for any state $x$, $x$ minimizes the quality of $C_1$ if and only if it minimizes the quality of $C_2$.
background
A display channel consists of an observation map from states to an observation space together with a quality function on observations; the induced state quality is the composition of these two maps. Quality equivalence is the relation asserting that any pair of states is ordered the same way under the two induced quality functions. The module sets display channels as the basic mechanism for projecting states into observation spaces, with optimality defined as global minimization of the induced quality function.
proof idea
The proof is a one-line term-mode construction of the biconditional. It builds the forward implication by applying the forward direction of the quality-equivalence hypothesis to the minimality statement for the first channel, and the reverse implication by applying the reverse direction to the minimality statement for the second channel.
why it matters in Recognition Science
This theorem is invoked by the optimal_transfer result in the OrderPreservation module. It supplies the invariance step that lets optimality be transferred across quality-equivalent channels inside the RRF core. The result ensures that the identification of optimal states remains stable under changes of observation channel, a prerequisite for consistent recognition across different projections.
scope and limits
- Does not establish criteria for when two channels are quality-equivalent.
- Does not address existence or uniqueness of optimal states.
- Does not extend the equivalence to channels that are not quality-equivalent.
- Does not treat computational or algorithmic aspects of checking optimality.
formal statement (Lean)
72theorem optimal_iff {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}
73 (heq : QualityEquiv C₁ C₂) (x : State) :
74 C₁.isOptimal x ↔ C₂.isOptimal x :=
proof body
Term-mode proof.
75 ⟨fun h1 y => (heq x y).mp (h1 y), fun h2 y => (heq x y).mpr (h2 y)⟩
76
77end QualityEquiv
78
79end RRF.Core
80end IndisputableMonolith