FullMultiplicativeLawOfLogicCert
plain-language theorem explainer
A certificate structure packaging the full recognizer-to-logic package on the positive multiplicative event space: identity, symmetry, and totality of the geometric cost; a separating primitive observer under nontrivial recognition; and (L4) composition consistency for the derived comparator cost, plain and polynomial d'Alembert form, plus identity at 1 and reciprocal symmetry. Cited by anyone using the honest conditional upgrade of (L4) under multiplicative structure. Pure structure definition whose fields are Prop obligations.
Claim. A full multiplicative law-of-logic certificate on a configuration type $\mathcal{C}$ is a record asserting, for every multiplicative recognizer $m$ on $\mathcal{C}$ (event space $\mathbb{R}_{>0}$ with a continuous Law-of-Logic comparator): the geometric cost vanishes on the diagonal, is symmetric, and is total; nontrivial recognition yields a primitive observer separating two distinct positive reals; the derived cost $F$ satisfies $F(xy)+F(x/y)=P(F(x),F(y))$ for some combiner $P$, and in the stronger polynomial degree-$\le 2$ form; and $F(1)=0$ with $F(x)=F(x^{-1})$ for $x>0$.
background
Module Foundation.MultiplicativeRecognizerL4 treats the honest form of (L4) Composition Consistency. The companion paper claimed any compositional recognizer on a multiplicative event space satisfies (L4) automatically; the equality-induced cost on $(\mathbb{R}_{>0},\cdot)$ refutes the unrestricted claim, so the module proves the conditional: pair a recognizer onto positive reals with a continuous comparator satisfying the Law of Logic, and (L4) becomes a theorem.
A multiplicative recognizer packages a geometric recognizer onto ${x:\mathbb{R}\mid 0<x}$, a continuous comparison operator, and a proof that the comparator satisfies the Law of Logic (Aristotelian conditions, scale invariance, non-triviality). Its derived cost is $F(r):=C(r,1)$. The polynomial form of (L4) asks for a symmetric combiner of total degree at most two with $F(xy)+F(x/y)=P(F(x),F(y))$, the shape produced by the d'Alembert inevitability route in LogicAsFunctionalEquation.
The three geometric fields (identity, non-contradiction, totality) are the definitional recognizer axioms. Primitive-observer existence links to ObserverFromRecognition: nontrivial recognition forces a separator on the positive reals.
proof idea
No proof body: this is a structure whose eight fields are Prop-valued obligations. Inhabitation is supplied downstream by fullMultiplicativeLawOfLogicCert, which fills each field by applying the corresponding lemma: geometric identity, non-contradiction, and totality from the underlying Recognizer; primitive-observer existence from the nontrivial-recognition hypothesis; multiplicative (L4) and its polynomial strengthening from the derivation theorems for multiplicative recognizers; identity at one and reciprocal symmetry from the comparator Law-of-Logic package. The companion theorem fullMultiplicativeLawOfLogicCert_inhabited is then a one-line Nonempty witness.
why it matters
This certificate is the paper-facing packaging of the module headline: under the multiplicative-event-space assumption, the substantive hypothesis RecognizerComposition (L4) becomes a derived theorem rather than an open interface. Downstream, fullMultiplicativeLawOfLogicCert builds a canonical inhabitant for every configuration type, and fullMultiplicativeLawOfLogicCert_inhabited records that no extra hypothesis beyond MultiplicativeRecognizer is required.
In the Recognition framework this sits at the logic-from-geometry bridge: the Recognition Composition Law and the d'Alembert form of route independence force a polynomial combiner of degree at most two on the positive multiplicative carrier, aligning with the J-cost functional equation lineage (T5 J-uniqueness and the RCL). It does not claim every recognizer satisfies (L4); it certifies the honest conditional that closes the gap between geometric recognition data and composition consistency when the carrier is $(\mathbb{R}_{>0},\cdot)$ with a Law-of-Logic comparator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.