multiplicativeRecognizer_satisfies_L4_polynomial
plain-language theorem explainer
Any multiplicative recognizer on the positive reals satisfies the polynomial form of (L4) composition consistency, so that its cost function obeys F(xy) + F(x/y) = P(F(x), F(y)) for a symmetric quadratic polynomial P. Researchers deriving logic from recognition geometry cite this to convert the composition-consistency hypothesis into a theorem once the event space is multiplicative and the comparator obeys the Law of Logic. The proof is a direct extraction of the polynomial witness and route map from the route_independence field of SatisfiesLaw
Claim. Let $m$ be a multiplicative recognizer. Then there exists a symmetric polynomial $P : ℝ → ℝ → ℝ$ of total degree at most two, $P(u,v) = a + b u + c v + d u v + e u^2 + f v^2$, such that for all positive reals $x,y$, $m.cost(x y) + m.cost(x/y) = P(m.cost x, m.cost y)$.
background
The module shows that (L4) Composition Consistency holds automatically for multiplicative recognizers. A MultiplicativeRecognizer pairs a geometric recognizer onto positive reals with a continuous comparison operator that satisfies the Law of Logic (Aristotelian conditions plus scale invariance and non-triviality). The derived cost is $F(r) := C(r,1)$ where $C$ is the comparator. MultiplicativeL4Polynomial asserts existence of a quadratic polynomial combiner $P$ that is symmetric and obeys the d'Alembert relation $F(xy) + F(x/y) = P(F(x), F(y))$. This rests on the route_independence property supplied by LogicAsFunctionalEquation, which guarantees such a polynomial under the Law of Logic.
proof idea
The proof obtains the polynomial $P$, its explicit quadratic form, symmetry, and the route equality directly from the route_independence field of $m.laws$. It then refines the MultiplicativeL4Polynomial structure by supplying $P$, the coefficient witness, symmetry, and the cost equality via the route map applied to positive $x,y$.
why it matters
This theorem supplies the polynomial form of (L4) used by l4DerivableCert and by the abstract multiplicativeRecognizer_satisfies_L4 theorem. It realizes the paper claim that any compositional recognizer on a multiplicative event space satisfies (L4) automatically once equipped with a Law-of-Logic comparator. In the Recognition Science framework it converts the composition-consistency hypothesis into a derived theorem for the positive-reals carrier, aligning with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.