MultiplicativeRecognizer
plain-language theorem explainer
MultiplicativeRecognizer packages a recognizer on positive reals with a Law-of-Logic comparator so that composition consistency (L4) becomes a derived theorem rather than a hypothesis. Researchers deriving route independence on multiplicative event spaces cite it to replace the RecognizerComposition assumption with an automatic result. The declaration is a structure definition that bundles the recognizer, comparator, and laws proof with no further obligations.
Claim. Let $C$ be a type. A multiplicative recognizer on $C$ consists of a recognizer $R$ from events in $C$ to positive reals, a continuous comparison operator $C$ on positive reals, and a proof that $C$ satisfies the Law of Logic (identity, reciprocity, transitivity, scale invariance, and non-triviality). The derived cost is then $F(r) := C(r,1)$.
background
In the Recognition Science setting a recognizer maps distinctions in a carrier type to costs via a comparison operator. The module restricts the event space to the positive reals under multiplication and replaces the default equality-induced cost (which fails (L4)) with one induced by a continuous comparator obeying the Law of Logic. Module documentation states that this pairing yields the d'Alembert form $F(xy)+F(x/y)=P(F(x),F(y))$ for the derived cost $F(r):=C(r,1)$ with a polynomial combiner of degree at most two, exactly as supplied by LogicAsFunctionalEquation.RouteIndependence.
proof idea
The declaration is a structure definition. It introduces the type by specifying three fields: the underlying geometric recognizer onto positive reals, the comparison operator, and the proof that the operator satisfies the Law of Logic. No lemmas or tactics are applied; the structure itself supplies the data needed for downstream derivations.
why it matters
This structure converts the (L4) substantive hypothesis into a theorem under the multiplicative-event-space assumption, directly feeding L4DerivableCert, L4_derivable_on_multiplicative_event_space, and the cost definitions. It implements the claim from RS_Recognition_Geometry_Logic_Unification.tex that any compositional recognizer family on a multiplicative carrier satisfies (L4) automatically. It touches the open question of which carriers make (L4) automatic versus those that require it as hypothesis, while remaining compatible with the Recognition Composition Law and J-uniqueness (T5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.