pith. machine review for the scientific record. sign in
def definition def or abbrev high

trivialChannelBundle

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  63def trivialChannelBundle : ChannelBundle TrivialState where
  64  Index := Unit

proof body

Definition body.

  65  Obs := fun _ => Unit
  66  channel := fun _ => trivialChannel
  67
  68/-- The trivial octave. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.