trivialChannelBundle
plain-language theorem explainer
The trivial channel bundle equips the single-point state space with a unit observation map and a constant trivial channel. Researchers verifying internal consistency of the RRF axiom system cite it as the base case before introducing dynamics or the phi-ladder. The definition proceeds by direct field assignment inside the ChannelBundle structure.
Claim. A channel bundle over the trivial state space $U$ (where $U$ is the unit type) is given by setting the index set to $U$, the observation map to the constant function returning $U$, and the channel map to the constant function returning the trivial channel.
background
The module builds the simplest model satisfying RRF axioms, with state space reduced to a single point, zero strain, and a trivially closed ledger. TrivialState is defined as the unit type. ChannelBundle is the structure imported from RRF.Core.DisplayChannel that packages an index set, an observation function, and a channel selector.
proof idea
The declaration is a direct definition. It assigns Index to Unit, Obs to the constant function returning Unit, and channel to the constant function returning trivialChannel.
why it matters
This supplies the channels component of trivialOctave, which assembles the complete trivial model and demonstrates consistency of the core RRF axioms. It serves as the base case prior to the forcing chain (T0-T8), the Recognition Composition Law, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.