 229  monotone : ∀ x y, V.strain.J x ≤ V.strain.J y → quality (observe x) ≥ quality (observe y)
 230
 231/-- Multiple display channels agree on quality ordering. -/
 232structure ChannelCoherence (V : VantageCategory) where
 233  /-- Indexed family of channels. -/
 234  channel : ℕ → Σ (Obs : Type*), DisplayFunctor V Obs
 235  /-- All channels agree: if x is better than y in channel i, same in channel j. -/
 236  coherent : ∀ i j : ℕ, ∀ x y : V.State,
 237    (channel i).2.quality ((channel i).2.observe x) >
 238    (channel i).2.quality ((channel i).2.observe y) ↔
 239    (channel j).2.quality ((channel j).2.observe x) >
 240    (channel j).2.quality ((channel j).2.observe y)
 241
 242/-! ## The One J Thesis -/
 243
 244/-- The One J Thesis (weak form): lower strain implies higher or equal quality.
 245
 246This is provable from the monotonicity constraint.
 247-/
 248theorem one_J_thesis_weak (V : VantageCategory) (Obs : Type*)
 249    (D : DisplayFunctor V Obs) :
 250    ∀ x y : V.State,
 251    V.strain.J x ≤ V.strain.J y →
 252    D.quality (D.observe x) ≥ D.quality (D.observe y) := by
 253  intro x y hJ
 254  exact D.monotone x y hJ
 255
 256/-- The One J Thesis (for coherent channels): channels agree on quality ordering.
 257
 258Given coherent channels, quality ordering is preserved across all channels.
 259-/
 260theorem one_J_thesis_coherent (V : VantageCategory) (coh : ChannelCoherence V)
 261    (i j : ℕ) (x y : V.State) :
 262    (coh.channel i).2.quality ((coh.channel i).2.observe x) >

papers checked against this theorem

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