multiplicativeRecognizer_satisfies_L4
Any multiplicative recognizer on positive reals with a continuous Law-of-Logic comparator automatically satisfies the multiplicative form of route-independence (L4). Recognition Science derivations would cite this to replace the composition-consistency hypothesis with a derived theorem once the event space is multiplicative. The proof is a one-line wrapper that extracts the existence statement from the polynomial version of the same result.
claimLet $m$ be a multiplicative recognizer. Then there exists a function $P : ℝ → ℝ → ℝ$ such that for all positive reals $x, y$, $m.cost(x · y) + m.cost(x / y) = P(m.cost x, m.cost y)$.
background
A MultiplicativeRecognizer pairs a geometric recognizer onto positive reals with a continuous comparison operator that satisfies the Law of Logic (all four Aristotelian conditions plus scale invariance). MultiplicativeL4 is the d'Alembert form of route independence: the cost of the product comparison plus the cost of the quotient comparison equals some combiner P evaluated on the component costs. The module derives this conditional theorem for the specific carrier (ℝ>0, ·) and continuous cost, contrasting with the equality-induced cost that fails (L4) on the same space. The upstream multiplicativeRecognizer_satisfies_L4_polynomial supplies the polynomial-degree-2 combiner from the route_independence field of SatisfiesLawsOfLogic.
proof idea
The term proof calls multiplicativeRecognizer_satisfies_L4_polynomial m to obtain the tuple containing P and the route property, then projects to the existence form of MultiplicativeL4 by discarding the polynomial and symmetry fields.
why it matters in Recognition Science
This supplies the existence statement used directly by the downstream L4_derivable_on_multiplicative_event_space. It converts the substantive hypothesis RecognizerComposition from the companion paper into a theorem under the multiplicative-event-space assumption, confirming automatic satisfaction of the d'Alembert form once the carrier and comparator are fixed as required.
scope and limits
- Does not establish (L4) for non-multiplicative event spaces or arbitrary recognizers.
- Does not compute or exhibit the explicit combiner P.
- Does not apply to discontinuous comparators or non-continuous costs.
- Does not address uniqueness of the combiner or higher-degree forms.
formal statement (Lean)
122theorem multiplicativeRecognizer_satisfies_L4
123 (m : MultiplicativeRecognizer 𝒞) :
124 MultiplicativeL4 m := by
proof body
Term-mode proof.
125 obtain ⟨P, _, _, hroute⟩ := multiplicativeRecognizer_satisfies_L4_polynomial m
126 exact ⟨P, hroute⟩
127
128/-- **The (L4) substantive hypothesis is derivable in the multiplicative case.**
129
130This is the headline theorem: the route-independence condition that the
131companion paper exposed as a hypothesis (`RecognizerComposition`) is in
132fact a theorem under the multiplicative-event-space structure. -/