L4_derivable_on_multiplicative_event_space
plain-language theorem explainer
Multiplicative recognizers on positive reals equipped with continuous comparators satisfying the laws of logic yield a cost function obeying the d'Alembert form of route-independence (L4). Researchers closing the hypothesis gap in Recognition Science derivations cite this result to replace RecognizerComposition with a derived statement. The proof is a direct one-line application of the polynomial satisfaction theorem that extracts the required combiner.
Claim. Let $m$ be a multiplicative recognizer. Then there exists a function $P : ℝ → ℝ → ℝ$ such that for all positive reals $x, y$, $F(xy) + F(x/y) = P(F(x), F(y))$, where $F$ is the cost induced by the comparator of $m$.
background
A multiplicative recognizer is the structure pairing a geometric recognizer whose event space is the positive reals under multiplication with a continuous comparison operator that satisfies SatisfiesLawsOfLogic. The induced cost is the derived cost of that comparator, which vanishes at the identity by the Identity law and obeys reciprocal symmetry by NonContradiction. The module works in the setting where the event space is $(ℝ_{>0}, ·)$ and the comparator is continuous and logic-satisfying, so that the d'Alembert form of (L4) becomes automatic for the derived cost $F(r) := C(r,1)$.
proof idea
The proof is a one-line wrapper that applies multiplicativeRecognizer_satisfies_L4. That lemma obtains the combiner polynomial from multiplicativeRecognizer_satisfies_L4_polynomial and packages the route-independence witness as the required existential statement.
why it matters
This declaration converts the substantive hypothesis RecognizerComposition from RecognizerInducesLogic into a theorem under the multiplicative-event-space assumption, matching the claim in RS_Recognition_Geometry_Logic_Unification.tex. It supplies the l4_from_recognizer field of l4DerivableCert. In the framework it secures the composition law required for the J-functional equation and the subsequent steps toward J-uniqueness (T5) and the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.