  55  ⟨trivial_balanced, trivial_ledger_closed⟩
  56
  57/-- Trivial display channel: observe nothing, quality always zero. -/
  58def trivialChannel : DisplayChannel TrivialState Unit where
  59  observe := fun _ => ()
  60  quality := fun _ => 0
  61
  62/-- Trivial channel bundle. -/
  63def trivialChannelBundle : ChannelBundle TrivialState where
  64  Index := Unit
  65  Obs := fun _ => Unit
  66  channel := fun _ => trivialChannel
  67
  68/-- The trivial octave. -/
  69def trivialOctave : Octave where
  70  State := TrivialState
  71  strain := trivialStrain
  72  channels := trivialChannelBundle
  73  inhabited := ⟨()⟩
  74
  75/-- The trivial octave is well-posed. -/
  76theorem trivialOctave_wellPosed : trivialOctave.wellPosed :=
  77  ⟨(), trivial_balanced⟩
  78
  79/-- The trivial model is consistent (nonempty at universe 0). -/
  80theorem trivialModel_consistent : Nonempty (Octave.{0, 0, 0}) := ⟨trivialOctave⟩
  81
  82/-! ## Vantage Triple in Trivial Model -/
  83
  84/-- A unified vantage triple in the trivial model. -/
  85def trivialVantageTriple : VantageTriple TrivialState :=
  86  VantageTriple.unified ()
  87
  88theorem trivialVantageTriple_unified : VantageTriple.isUnified trivialVantageTriple :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.