IndisputableMonolith.RRF.Models.Trivial

   1import IndisputableMonolith.RRF.Core
   2
   3/-!
   4# RRF Models: Trivial Model
   5
   6The simplest possible model that satisfies RRF axioms.
   7
   8State = Unit (one state)
   9J = 0 (always balanced)
  10Ledger = 0/0 (trivially closed)
  11
  12This proves internal consistency of the core axiom bundle.
  13-/
  14
  15
  16namespace IndisputableMonolith
  17namespace RRF.Models
  18
  19open RRF.Core
  20
  21/-! ## The Trivial Model -/
  22
  23/-- Trivial state space: a single point. -/
  24abbrev TrivialState := Unit
  25
  26/-- Trivial strain: always zero. -/
  27def trivialStrain : StrainFunctional TrivialState where
  28  J := fun _ => 0
  29
  30instance : StrainFunctional.NonNeg trivialStrain where
  31  nonneg := fun _ => le_refl 0
  32
  33/-- The single state is balanced. -/
  34theorem trivial_balanced : trivialStrain.isBalanced () := rfl
  35
  36/-- The single state is a minimizer. -/
  37theorem trivial_is_minimizer : trivialStrain.isMinimizer () :=
  38  StrainFunctional.equilibria_are_minimizers () trivial_balanced
  39
  40/-- Trivial ledger: zero debit and credit. -/
  41def trivialLedger : LedgerConstraint TrivialState where
  42  debit := fun _ => 0
  43  credit := fun _ => 0
  44
  45/-- Trivial ledger is closed. -/
  46theorem trivial_ledger_closed : trivialLedger.isClosed () := rfl
  47
  48/-- Trivial strain-ledger system. -/
  49def trivialStrainLedger : StrainLedger TrivialState where
  50  strain := trivialStrain
  51  ledger := trivialLedger
  52
  53/-- The trivial state is valid. -/
  54theorem trivial_is_valid : trivialStrainLedger.isValid () :=
  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 :=
  89  VantageTriple.unified_is_unified ()
  90
  91end RRF.Models
  92end IndisputableMonolith
  93