refl
plain-language theorem explainer
Reflexivity of quality equivalence asserts that any display channel induces the same weak ordering on states as itself. Modelers constructing equivalence classes of observation maps for discrete fluid states would invoke this to close the relation. The proof is a direct term-mode reduction to the reflexivity of the biconditional.
Claim. For every display channel $C$ from a state space to an observation space, the induced quality ordering satisfies $C.stateQuality(x) ≤ C.stateQuality(y) ↔ C.stateQuality(x) ≤ C.stateQuality(y)$ for all states $x, y$.
background
A display channel is a structure pairing an observation map from states to observations with a real-valued quality function on observations; the derived stateQuality composes these to assign reals directly to states. QualityEquiv declares two channels equivalent precisely when their stateQuality functions induce identical orderings on the state space. The module sets this in the core RRF layer for projecting states into observation spaces, with upstream State types drawn from discrete 2D Galerkin and vorticity lattice structures.
proof idea
The proof is a one-line term-mode wrapper: it abstracts over the pair of states and returns the reflexivity of logical equivalence.
why it matters
This reflexivity result supplies the first leg of the equivalence relation on display channels, pairing with the sibling symmetry and transitivity declarations to support quotient constructions. It fills the basic identity step in the RRF core before optimality predicates are applied to channels. No open questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.