trans
plain-language theorem explainer
Quality equivalence of display channels is transitive. Researchers comparing observation projections in discrete fluid models cite this to chain multiple channels while preserving state orderings. The proof is a one-line term applying biconditional transitivity pointwise to the two given equivalences.
Claim. Let $C_1$, $C_2$, $C_3$ be display channels over a common state space. If the quality functions of $C_1$ and $C_2$ induce identical orderings on all pairs of states and likewise for $C_2$ and $C_3$, then $C_1$ and $C_3$ induce identical orderings.
background
A display channel consists of an observation map from a state to an observation together with a real-valued quality on observations; the derived stateQuality ranks states by composing these maps. QualityEquiv holds precisely when two channels produce the same ordering: for every pair of states the inequality on one channel's stateQuality is equivalent to the inequality on the other's. The module sets display channels as projections of states into observation spaces for quality assessment in discrete models. Upstream State types supply the concrete instances: the discrete 2D Galerkin state from CPM2D and the finite vorticity field from DiscreteVorticity.
proof idea
The term proof evaluates the two QualityEquiv hypotheses at each pair of states and composes their biconditionals via the transitivity of logical equivalence.
why it matters
This completes the equivalence-relation axioms for QualityEquiv alongside the sibling refl and symm declarations, enabling the optimal_iff theorem that equates optimality across equivalent channels. It supports consistent quality comparisons when swapping observation projections in RRF fluid models without changing the induced ordering on states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.