IndisputableMonolith.RRF.Core.DisplayChannel

   1import Mathlib.Order.Basic
   2import Mathlib.Data.Real.Basic
   3
   4/-!
   5# RRF Core: Display Channel
   6
   7A display channel is a way of "observing" or "projecting" a state into an observation space.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace RRF.Core
  12
  13/-- A display channel from State to Observation. -/
  14structure DisplayChannel (State Obs : Type*) where
  15  observe : State → Obs
  16  quality : Obs → ℝ
  17
  18namespace DisplayChannel
  19
  20variable {State Obs : Type*}
  21
  22/-- The composed quality function: State → ℝ. -/
  23def stateQuality (C : DisplayChannel State Obs) : State → ℝ :=
  24  C.quality ∘ C.observe
  25
  26/-- A state is optimal in channel C if it minimizes quality. -/
  27def isOptimal (C : DisplayChannel State Obs) (x : State) : Prop :=
  28  ∀ y, C.stateQuality x ≤ C.stateQuality y
  29
  30end DisplayChannel
  31
  32/-- A collection of display channels on the same state space. -/
  33structure ChannelBundle (State : Type*) where
  34  Index : Type*
  35  Obs : Index → Type*
  36  channel : (i : Index) → DisplayChannel State (Obs i)
  37
  38namespace ChannelBundle
  39
  40variable {State : Type*}
  41
  42def isGloballyOptimal (B : ChannelBundle State) (x : State) : Prop :=
  43  ∀ i, (B.channel i).isOptimal x
  44
  45end ChannelBundle
  46
  47/-- Two channels are quality-equivalent if they induce the same ordering on states. -/
  48abbrev QualityEquiv {State Obs₁ Obs₂ : Type*}
  49    (C₁ : DisplayChannel State Obs₁)
  50    (C₂ : DisplayChannel State Obs₂) : Prop :=
  51  ∀ x y : State, C₁.stateQuality x ≤ C₁.stateQuality y ↔
  52                  C₂.stateQuality x ≤ C₂.stateQuality y
  53
  54namespace QualityEquiv
  55
  56variable {State Obs₁ Obs₂ Obs₃ : Type*}
  57
  58theorem refl (C : DisplayChannel State Obs₁) : QualityEquiv C C :=
  59  fun _ _ => Iff.rfl
  60
  61theorem symm {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}
  62    (h : QualityEquiv C₁ C₂) : QualityEquiv C₂ C₁ :=
  63  fun x y => (h x y).symm
  64
  65theorem trans {C₁ : DisplayChannel State Obs₁}
  66    {C₂ : DisplayChannel State Obs₂}
  67    {C₃ : DisplayChannel State Obs₃}
  68    (h₁₂ : QualityEquiv C₁ C₂) (h₂₃ : QualityEquiv C₂ C₃) : QualityEquiv C₁ C₃ :=
  69  fun x y => (h₁₂ x y).trans (h₂₃ x y)
  70
  71/-- Quality-equivalent channels have the same optimal states. -/
  72theorem optimal_iff {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}
  73    (heq : QualityEquiv C₁ C₂) (x : State) :
  74    C₁.isOptimal x ↔ C₂.isOptimal x :=
  75  ⟨fun h1 y => (heq x y).mp (h1 y), fun h2 y => (heq x y).mpr (h2 y)⟩
  76
  77end QualityEquiv
  78
  79end RRF.Core
  80end IndisputableMonolith
  81