symm
plain-language theorem explainer
Quality equivalence of display channels is symmetric: if channel C1 induces the same state ordering as C2 then the converse holds. Workers on equivalence classes of observation maps in discrete fluid models cite this to treat the relation as undirected. The proof is a one-line term that applies symmetry to the biconditional ordering predicate.
Claim. Let $C_1$ and $C_2$ be display channels from a common state space. If for all states $x,y$ the inequality $C_1$.stateQuality$(x) ≤ C_1$.stateQuality$(y)$ holds if and only if $C_2$.stateQuality$(x) ≤ C_2$.stateQuality$(y)$, then the converse biconditional also holds.
background
DisplayChannel is a structure with an observe map from State to Obs and a quality map from Obs to the reals; stateQuality denotes the composition quality ∘ observe. QualityEquiv is the proposition that two channels induce identical orderings on states via their stateQuality functions. The module defines display channels as projections of states into observation spaces for consistent quality assessment.
proof idea
one-line wrapper that applies symmetry of the biconditional to the hypothesis for each pair of states.
why it matters
This result completes the symmetry leg of QualityEquiv, which with the sibling reflexivity and transitivity declarations shows the relation is an equivalence. It supports partitioning display channels into classes that preserve state orderings in RRF models built on discrete vorticity and Galerkin states. No direct link to the T0-T8 chain appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.