multiplicative_reciprocal_symmetry
plain-language theorem explainer
The theorem establishes that the cost function derived from a multiplicative recognizer on the positive reals is invariant under reciprocation. Researchers deriving the Recognition Composition Law from the Law of Logic would cite this when confirming symmetry of the cost functional. The proof is a short term-mode chain that applies non-contradiction twice and scale invariance once, together with algebraic cancellation of inverses.
Claim. Let $m$ be a multiplicative recognizer on the positive reals equipped with comparison operator $C$. For every $x > 0$, the derived cost satisfies $C(x,1) = C(x^{-1},1)$.
background
A MultiplicativeRecognizer pairs a recognizer onto the positive reals with a continuous comparison operator satisfying the Law of Logic (Aristotelian conditions plus scale invariance and non-triviality). The derived cost is the function $F(r) := C(r,1)$. The module derives the d'Alembert form of the Recognition Composition Law (L4) automatically on this carrier: $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$. This rests on the Composition class from CostAxioms, which encodes the multiplicative consistency axiom, and on LedgerFactorization of the positive reals under multiplication.
proof idea
The term proof first invokes non-contradiction to equate $C(x,1)$ with $C(1,x)$. Scale invariance is then applied with scaling factor $x^{-1}$, yielding $C(1,x^{-1}) = C(x,1)$ after cancellation via inv_mul_cancel and mul_one. A second non-contradiction step on the reciprocal equates $C(x^{-1},1)$ with $C(1,x^{-1})$, closing the chain.
why it matters
The result supplies the reciprocal symmetry clause inside l4DerivableCert, which assembles the full certificate that any MultiplicativeRecognizer satisfies (L4). It thereby converts the abstract RecognizerComposition hypothesis into a derived theorem for the multiplicative event space, as claimed in the companion paper. The symmetry follows directly from the Law of Logic axioms and supports the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.