L4DerivableCert

formal source

 182not a hypothesis on a recognizer; it is a derived theorem whenever the
 183recognizer's event space is the positive reals under multiplication and
 184the comparator satisfies the Law of Logic. -/
 185structure L4DerivableCert (𝒞 : Type*) where
 186  l4_from_recognizer :
 187    ∀ m : MultiplicativeRecognizer 𝒞,
 188      ∃ P : ℝ → ℝ → ℝ,
 189        ∀ x y : ℝ, 0 < x → 0 < y →
 190          m.cost (x * y) + m.cost (x / y) = P (m.cost x) (m.cost y)
 191  l4_polynomial_form :
 192    ∀ m : MultiplicativeRecognizer 𝒞,
 193      MultiplicativeL4Polynomial m
 194  identity_at_one :
 195    ∀ m : MultiplicativeRecognizer 𝒞, m.cost 1 = 0
 196  reciprocal_symmetry :
 197    ∀ m : MultiplicativeRecognizer 𝒞,
 198      ∀ x : ℝ, 0 < x → m.cost x = m.cost (x⁻¹)
 199
 200def l4DerivableCert (𝒞 : Type*) : L4DerivableCert 𝒞 where
 201  l4_from_recognizer := fun m => L4_derivable_on_multiplicative_event_space m
 202  l4_polynomial_form := fun m => multiplicativeRecognizer_satisfies_L4_polynomial m
 203  identity_at_one := fun m => multiplicative_identity m
 204  reciprocal_symmetry := fun m => multiplicative_reciprocal_symmetry m
 205
 206theorem l4DerivableCert_inhabited (𝒞 : Type*) :
 207    Nonempty (L4DerivableCert 𝒞) :=
 208  ⟨l4DerivableCert 𝒞⟩
 209
 210end MultiplicativeRecognizer
 211
 212/-! ## Summary
 213
 214The substantive (L4) Composition Consistency condition is no longer an
 215assumed hypothesis on a recognizer. Whenever: