fullMultiplicativeLawOfLogicCert
plain-language theorem explainer
Packages a full multiplicative recognizer-to-logic certificate for every configuration type: identity, non-contradiction, totality, primitive observer, and multiplicative (L4) in polynomial d'Alembert form, plus identity at 1 and reciprocal symmetry. Cited by anyone upgrading the paper claim that composition consistency is automatic under multiplicative structure. Pure field-by-field assembly of prior recognizer laws and the multiplicative L4 theorems.
Claim. For every configuration type $\mathcal{C}$, a full multiplicative law-of-logic certificate exists: every multiplicative recognizer on $\mathcal{C}$ has cost vanishing on the diagonal, symmetric under swap, total, induces a primitive observer, and its derived cost $F(r)=C(r,1)$ obeys $F(xy)+F(x/y)=P(F(x),F(y))$ for some polynomial combiner $P$ of degree at most two, with $F(1)=0$ and $F(x)=F(x^{-1})$.
background
Module setting: RecognizerInducesLogic left (L4) Composition Consistency as a substantive hypothesis. The companion paper claimed any compositional recognizer on a multiplicative event space satisfies (L4) automatically. This module formalises the honest conditional: if a recognizer is paired with a continuous Law-of-Logic comparator $C$ on $(\mathbb{R}_{>0},\cdot)$, then the d'Alembert form $F(xy)+F(x/y)=P(F(x),F(y))$ holds for $F(r):=C(r,1)$ with $\deg P\le 2$.
A multiplicative recognizer pairs a geometric recognizer onto positive reals with a continuous comparison operator satisfying all four Aristotelian laws. The default equality-induced cost fails (L4) on this carrier; the right cost makes (L4) a theorem.
The structure being inhabited collects three definitional recognizer conditions, primitive-observer induction, multiplicative (L4) existence, the polynomial form, comparator identity at one, and reciprocal symmetry.
proof idea
Definitional record construction, not a tactic proof. Each field is a one-line projection or application:
- identity, non-contradiction, totality:
Recognizer.identity,.non_contradiction,.totalityonm.recognizer; - primitive observer:
Recognizer.induces_primitive_observer; - multiplicative (L4):
L4_derivable_on_multiplicative_event_space(headline theorem reducing tomultiplicativeRecognizer_satisfies_L4); - polynomial form:
multiplicativeRecognizer_satisfies_L4_polynomial; - comparator identity at 1 and reciprocal symmetry:
multiplicative_identityandmultiplicative_reciprocal_symmetry(from the comparator's Law-of-Logic axioms plus scale invariance).
why it matters
Closes the paper-upgrade path: the certificate is inhabited with no hypothesis beyond MultiplicativeRecognizer. Downstream, fullMultiplicativeLawOfLogicCert_inhabited is the one-line Nonempty witness built from this def.
In the Recognition framework this converts the old RecognizerComposition hypothesis into a derived theorem on the multiplicative carrier, aligning the formal ledger with the companion paper's claim that route-independence (the d'Alembert/RCL shape behind J-cost uniqueness in the T5 forcing step) is automatic once the event space is $(\mathbb{R}_{>0},\cdot)$ with a Law-of-Logic comparator. It does not revive the false universal claim that every recognizer satisfies (L4).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.