DisplayChannel
plain-language theorem explainer
DisplayChannel pairs an observation map from a state space to an observation space with a real-valued quality function on the observations. Researchers formalizing optimality criteria in discrete fluid models cite it when defining projection-based quality assessments. The declaration is the structure definition itself, which directly enables the composed stateQuality function and all downstream equivalence and optimality predicates.
Claim. For a state space $S$ and observation space $O$, a display channel consists of an observation map $observe : S → O$ together with a quality function $quality : O → ℝ$.
background
The RRF core module defines display channels as projections that turn states into observations equipped with a quality value. The module doc states that a display channel is a way of observing or projecting a state into an observation space. Upstream, CPM2D.State is the discrete 2D Galerkin state type at truncation level N, while DiscreteVorticity.State is a finite discrete vorticity field on a lattice window of siteCount sites; these supply the concrete state types to which channels are applied.
proof idea
The declaration is the structure definition itself. It introduces the two fields observe and quality, which are used immediately to define the composed stateQuality function as quality ∘ observe in the same namespace.
why it matters
DisplayChannel is the base structure for the RRF display framework. It is used to build ChannelBundle as collections of channels on one state space and to define isOptimal (states that minimize quality) together with QualityEquiv (channels that induce identical orderings). Theorems optimal_iff, refl, symm and trans all rest on it. This bridges discrete fluid states from Navier-Stokes discretizations to optimality notions inside the Recognition Science setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.