 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:
 216
 217* the recognizer's event space is the positive reals under multiplication,
 218* the comparator on that space satisfies the Law of Logic in operator form,
 219
 220then the route-independence field of `SatisfiesLawsOfLogic` directly
 221supplies a polynomial-degree-2 combiner realising (L4). The geometric
 222primitive (recognizer) plus the cost-functional primitive (Law of Logic
 223on positive ratios) jointly force the d'Alembert composition law.
 224
 225This closes the L4 frontier identified by
 226`RecognizerInducesLogic.RecognizerComposition` for the multiplicative case.
 227The substantive content was always in the comparator's compositional
 228structure, not in the recognizer's set-theoretic shape.
 229-/
 230

papers checked against this theorem

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