trivialOctave
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not model any physical system or yield observable predictions.
- Does not incorporate the phi-ladder, mass formulas, or Berry threshold.
- Does not address the alpha band or spatial dimension forcing.
- Does not claim to be the only possible Octave instance.
Lean usage
theorem trivialModel_consistent : Nonempty (Octave.{0, 0, 0}) := ⟨trivialOctave⟩formal statement (Lean)
69def trivialOctave : Octave where
70 State := TrivialState
proof body
Definition body.
71 strain := trivialStrain
72 channels := trivialChannelBundle
73 inhabited := ⟨()⟩
74
75/-- The trivial octave is well-posed. -/