l4DerivableCert
plain-language theorem explainer
Any multiplicative recognizer on the positive reals yields a cost function satisfying the d'Alembert form of composition consistency (L4). Researchers formalizing the derivation of logic from recognition would cite the certificate to replace an independent hypothesis with a derived property. The definition is assembled by wiring four prior theorems directly into the fields of the L4DerivableCert structure.
Claim. Let $𝒞$ be a type. An $L4DerivableCert$ $𝒞$ is the record whose four fields are maps on multiplicative recognizers $m$: the map sending $m$ to a witness that $m.cost(xy) + m.cost(x/y) = P(m.cost x, m.cost y)$ for some $P:ℝ→ℝ→ℝ$; the map sending $m$ to a proof that $m$ satisfies the multiplicative L4 polynomial condition; the map sending $m$ to a proof that $m.cost(1)=0$; and the map sending $m$ to a proof that $m.cost x = m.cost(x^{-1})$ for all $x>0$.
background
A MultiplicativeRecognizer pairs a comparator $C$ on $(ℝ_{>0},·)$ with a SatisfiesLawsOfLogic operator whose route-independence field supplies a quadratic combiner. The derived cost is $F(r):=C(r,1)$. Under this structure the d'Alembert equation $F(xy)+F(x/y)=P(F(x),F(y))$ holds automatically, converting the abstract RecognizerComposition hypothesis into a theorem (see MODULE_DOC).
proof idea
This is a definition that constructs an instance of the L4DerivableCert structure by supplying explicit functions for each field. The l4_from_recognizer field is populated by L4_derivable_on_multiplicative_event_space, the l4_polynomial_form field by multiplicativeRecognizer_satisfies_L4_polynomial, the identity_at_one field by multiplicative_identity, and the reciprocal_symmetry field by multiplicative_reciprocal_symmetry.
why it matters
The definition supplies the concrete inhabitant required by the downstream theorem l4DerivableCert_inhabited, which asserts Nonempty (L4DerivableCert 𝒞). It thereby converts the paper claim that (L4) follows from multiplicative structure into a formal result, removing RecognizerComposition as an independent hypothesis in this case and supporting the Recognition Composition Law step in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.