L4DerivableCert
plain-language theorem explainer
L4DerivableCert packages the four properties that certify automatic derivation of (L4) composition consistency once a recognizer is restricted to the positive reals under multiplication with a Law-of-Logic comparator. Researchers tracing the Recognition Science derivation of functional equations would cite it to replace the general RecognizerComposition hypothesis with a theorem under the multiplicative carrier. The structure is assembled by direct application of four sibling lemmas that establish the combiner P, its quadratic polynomial shape,
Claim. Let $m$ be a multiplicative recognizer. Then there exists $P : ℝ → ℝ → ℝ$ such that for all $x,y > 0$, $m.cost(xy) + m.cost(x/y) = P(m.cost x, m.cost y)$, the map $P$ is a symmetric polynomial of total degree at most two, $m.cost(1) = 0$, and $m.cost(x) = m.cost(x^{-1})$ for every $x > 0$.
background
A multiplicative recognizer pairs a geometric recognizer onto the positive reals with a continuous comparison operator that satisfies the Law of Logic (all four Aristotelian conditions plus scale invariance). Its cost is the derived cost of that comparator, coinciding with the J-cost of the underlying recognition event. The module works inside the setting where the event space is (ℝ>0, ·) and the comparator is continuous, so that the d'Alembert form of (L4) becomes provable rather than postulated.
proof idea
The declaration is a pure structure definition with four fields. Downstream construction applies L4_derivable_on_multiplicative_event_space to obtain the combiner P, multiplicativeRecognizer_satisfies_L4_polynomial to obtain the quadratic form, multiplicative_identity to obtain the value at unity, and multiplicative_reciprocal_symmetry to obtain reciprocal invariance. No tactics or reductions are required.
why it matters
The structure supplies the certificate that (L4) is automatic for multiplicative recognizers, directly feeding the construction of l4DerivableCert and the inhabitedness theorem. It realizes the honest conditional claimed in the companion paper: once the carrier is multiplicative and the comparator obeys the Law of Logic, the Recognition Composition Law holds in d'Alembert form with a quadratic combiner. This step supports the forcing-chain derivation of composition laws from J-uniqueness without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.