ChannelBundle
plain-language theorem explainer
ChannelBundle packages multiple display channels that share one common state space, enabling uniform optimality checks and octave-level observation models. Workers on the RRF observation layer cite it when building multi-projection structures for strain or quality comparisons. The declaration is a plain structure definition that directly assembles an index set, a family of observation types, and the corresponding DisplayChannel instances.
Claim. Let $S$ be a state space. A channel bundle over $S$ consists of an index set $I$, a family of observation spaces $(O_i)_{i : I}$, and a map sending each $i$ to a display channel $C_i : S → O_i$ equipped with a quality function $O_i → ℝ$.
background
In the RRF core module a display channel is a pair consisting of an observe map from state to observation together with a real-valued quality function on the observation space. The module treats these channels as the basic projectors that turn raw states into comparable observations. ChannelBundle collects several such channels over one fixed state space so that global properties such as optimality can be stated uniformly across all channels. The upstream DisplayChannel structure supplies the observe and quality fields; concrete state spaces are drawn from discrete fluid models and relativity index conventions.
proof idea
This is a structure definition that directly declares the three fields Index, Obs, and channel. No lemmas or tactics are invoked; the construction is the primitive packaging of a family of DisplayChannel instances.
why it matters
The structure is required by the Octave definition in RRF.Core.Octave, which combines a strain functional with a collection of display channels. It is used to define isGloballyOptimal, which asserts that a state is optimal for every channel in the bundle, and appears in the trivial model construction. Within the Recognition framework it supplies the multi-channel observation layer at each octave without yet introducing the J-cost, phi-ladder, or eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.