isGloballyOptimal
plain-language theorem explainer
A state x is globally optimal for a bundle B of display channels if it minimizes the quality function in every channel of the bundle. Researchers modeling multi-view state observation in RRF would cite this when proving consistency across projections. The declaration is a direct one-line abbreviation that applies the single-channel optimality predicate universally over the bundle index set.
Claim. Given a collection $B$ of display channels on a common state space $S$, a state $x$ in $S$ is globally optimal if, for every channel $C_i$ in the collection, $x$ minimizes the state quality function of $C_i$.
background
Display channels project states into observation spaces and equip each projection with a stateQuality function returning a real-valued cost. A ChannelBundle assembles multiple such channels that share the same underlying state type, with an Index set and a map from indices to individual channels. The isOptimal predicate on a single channel states that a state achieves the global minimum of that channel's quality function. Upstream results supply concrete State types from 2D fluid models (Galerkin truncation and discrete vorticity lattices) that instantiate these channels.
proof idea
The definition is a one-line wrapper that applies the isOptimal predicate to each channel in the bundle via universal quantification over the Index type.
why it matters
This definition supplies the basic vocabulary for optimality across multiple observation channels in the RRF core. It prepares statements about states that remain optimal under every projection in the bundle, aligning with the Recognition Science emphasis on unique fixed points under composed maps. No downstream theorems yet invoke it, leaving open the question of existence and uniqueness results for globally optimal states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.