optimal_iff
plain-language theorem explainer
Quality-equivalent display channels share identical optimal states. Researchers transferring optimality results across projections in RRF models cite this equivalence. The proof is a direct term-mode biconditional built from the forward and reverse directions of the QualityEquiv hypothesis.
Claim. If display channels $C_1$ and $C_2$ are quality-equivalent, i.e., $C_1.stateQuality(x) ≤ C_1.stateQuality(y) ↔ C_2.stateQuality(x) ≤ C_2.stateQuality(y)$ for all states $x,y$, then for any state $x$ we have $C_1.isOptimal(x) ↔ C_2.isOptimal(x)$.
background
DisplayChannel is the structure with fields observe : State → Obs and quality : Obs → ℝ; stateQuality composes them into a real-valued function on State. QualityEquiv is the proposition that two such channels on the same State induce identical orderings on states. isOptimal asserts that a state globally minimizes the composed quality function. The module presents display channels as projections from states into observation spaces within the RRF setting. Upstream definitions include RRF as a local non-sealed recognition field and State types from discrete fluid and vorticity models.
proof idea
The proof is a one-line term-mode wrapper. It constructs the forward direction by applying the mp implication of heq pointwise to the optimality quantifier, and the reverse direction by applying mpr in the same way.
why it matters
This result is invoked by the optimal_transfer theorem in RRF.Theorems.OrderPreservation, which restates the identical claim. It enables transfer of optimality across equivalent channels inside the RRF core and aligns with the recognition composition law. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.