recognition_is_cost_structure

formal source

  56  linarith
  57
  58/-- Recognition is cost structure. -/
  59theorem recognition_is_cost_structure :
  60    ∀ (e : LedgerForcing.RecognitionEvent),
  61    (e.ratio = 1 ↔ recognition_cost e = 0) ∧
  62    (e.ratio ≠ 1 → recognition_cost e > 0) := by
  63  intro e
  64  refine ⟨⟨self_recognition_zero_cost e, ?_⟩, nontrivial_recognition_positive_cost e⟩
  65  intro h
  66  simp only [recognition_cost, LedgerForcing.J] at h
  67  have hpos := e.ratio_pos
  68  have h0 : e.ratio ≠ 0 := hpos.ne'
  69  -- h says (e.ratio + e.ratio⁻¹)/2 - 1 = 0
  70  -- So e.ratio + e.ratio⁻¹ = 2
  71  have h1 : e.ratio + e.ratio⁻¹ = 2 := by linarith
  72  -- This means (e.ratio - 1)² = 0
  73  have heq : e.ratio + e.ratio⁻¹ = (e.ratio^2 + 1) / e.ratio := by field_simp
  74  have h2 : (e.ratio^2 + 1) / e.ratio = 2 := by rw [← heq]; exact h1
  75  have h3 : e.ratio^2 + 1 = 2 * e.ratio := by
  76    have := congrArg (· * e.ratio) h2
  77    simp only [div_mul_cancel₀ _ h0] at this
  78    linarith
  79  have h4 : (e.ratio - 1)^2 = 0 := by nlinarith [sq_nonneg (e.ratio - 1)]
  80  exact sub_eq_zero.mp (sq_eq_zero_iff.mp h4)
  81
  82/-! ## Part 1: Observable Extraction = Recognition -/
  83
  84structure Observable (S : Type) where
  85  value : S → ℝ
  86
  87structure ObservableExtractionMechanism (S : Type) where
  88  extract : S → ℝ
  89  nonconstant : ∃ s₁ s₂ : S, extract s₁ ≠ extract s₂