multiplicativeRecognizer_satisfies_L4
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Geometry rebuilt as a quotient of what measurements can distinguish
"Theorem 4: The recognition quotient of the composite refines the quotients of its components ... π_1 : C_{R_1⊗R_2} ↠ C_{R_1} and π_2 : C_{R_1⊗R_2} ↠ C_{R_2}"