MultiplicativeL4Polynomial
plain-language theorem explainer
MultiplicativeL4Polynomial packages the claim that any multiplicative recognizer admits a symmetric quadratic polynomial combiner for its cost that satisfies the multiplicative d'Alembert form of L4. Researchers deriving logic from recognition structures cite it when converting the route-independence axiom into an explicit polynomial equation on positive reals. The definition directly encodes existence of coefficients a through f together with the functional equation that matches the cost addition rule.
Claim. Let $m$ be a multiplicative recognizer. Then $m$ satisfies the polynomial L4 property when there exists a map $P:ℝ→ℝ→ℝ$ such that $P(u,v)=a+bu+cv+duv+eu^2+fv^2$ for some real $a,b,c,d,e,f$, $P$ is symmetric, and $m.cost(xy)+m.cost(x/y)=P(m.cost(x),m.cost(y))$ holds for all positive reals $x,y$.
background
The module works inside the multiplicative event space $(ℝ_{>0},·)$. A MultiplicativeRecognizer pairs a geometric recognizer onto positive reals with a continuous comparison operator whose laws field contains the four Aristotelian conditions plus scale invariance and route independence. The cost is obtained by applying the derivedCost construction to that operator, yielding a one-argument function on positive ratios. Upstream, SatisfiesLawsOfLogic supplies the route_independence component that already produces a quadratic combiner; the module documentation states that this yields the d'Alembert form $F(xy)+F(x/y)=P(F(x),F(y))$ automatically once the carrier is multiplicative.
proof idea
The declaration is the definition itself. It states the existence of a total-degree-2 polynomial $P$ that is symmetric and reproduces the cost addition identity. The downstream theorem multiplicativeRecognizer_satisfies_L4_polynomial obtains the polynomial and symmetry directly from the route_independence field of the laws structure and then verifies the functional equation by substitution of the cost definition.
why it matters
This definition is the target of the theorem multiplicativeRecognizer_satisfies_L4_polynomial and supplies the polynomial form required by the L4DerivableCert structure. It converts the earlier hypothesis RecognizerComposition into a derived result under the multiplicative assumption, exactly as claimed in the companion paper. The construction aligns with the d'Alembert Inevitability Theorem that forces the quadratic combiner once route independence is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.