trivialOctave
plain-language theorem explainer
The trivial octave supplies the minimal concrete Octave instance in the RRF framework by taking a singleton state space. Researchers checking internal consistency of the core RRF axioms cite it as the base witness for nonemptiness. The definition is a direct structure construction that assigns the trivial state, zero strain, and trivial channel bundle.
Claim. The trivial octave is the structure with state space the singleton set, strain function identically zero, channels given by the trivial bundle, and inhabited by the unique element of the singleton.
background
The RRF.Models.Trivial module presents the simplest model satisfying RRF axioms: state space reduced to a single point (Unit), J-cost identically zero (always balanced), and ledger trivially closed. This construction serves as an internal consistency check for the axiom bundle. Upstream, the Octave type is supplied by definitions in MusicalScale and Constants that fix the octave ratio to 2 and the period to eight ticks; TrivialState is the abbrev for Unit.
proof idea
The definition is a direct structure literal that populates the four fields of Octave: State is set to TrivialState, strain to trivialStrain, channels to trivialChannelBundle, and inhabited to the unit element.
why it matters
This definition provides the witness for trivialModel_consistent, which proves Nonempty (Octave.{0,0,0}), and for trivialOctave_wellPosed. It closes the consistency argument for the trivial model inside the Recognition framework and supplies the base case for the eight-tick octave structure. It touches the open question of whether nontrivial models exist that still satisfy the full axiom set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.