multiplicative_identity
plain-language theorem explainer
The derived cost for a multiplicative recognizer vanishes at the multiplicative identity. Researchers formalizing Recognition Science's derivation of composition consistency from logic axioms would cite this as the base case for the L4 functional equation on positive reals. The proof is a direct one-line application of the identity axiom inside the SatisfiesLawsOfLogic structure to the comparator at unity.
Claim. Let $m$ be a multiplicative recognizer on the positive reals equipped with comparison operator $C$ satisfying the Law of Logic. If $F(r) := C(r,1)$ denotes the induced cost, then $F(1) = 0$.
background
A multiplicative recognizer consists of a geometric recognizer onto the positive reals together with a continuous comparison operator obeying the Law of Logic (all four Aristotelian conditions plus scale invariance and non-triviality). The induced cost is the derived cost $F(r) := C(r,1)$ extracted from this operator. The module establishes the honest conditional that such recognizers automatically satisfy the d'Alembert form of (L4) on the multiplicative event space, in contrast to the equality-induced cost which fails (L4) outright.
proof idea
The proof is a one-line wrapper. It rewrites the cost at 1 as the comparator applied to the pair (1,1), then invokes the identity axiom from the SatisfiesLawsOfLogic component of the recognizer, with a normalization step confirming the argument equals 1.
why it matters
This supplies the identity_at_one field inside the L4DerivableCert certificate that aggregates all required properties for a multiplicative recognizer to derive (L4). It corresponds to the (L1) Identity clause in the module's formalization of composition consistency. Within the Recognition Science framework it anchors the functional equation for costs on the positive reals, supporting the route to the phi-ladder and the forcing chain from T5 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.