cost
plain-language theorem explainer
This definition supplies the cost function induced by any multiplicative recognizer by delegating directly to the derived cost of its comparator on positive ratios. Researchers deriving action principles or acoustic thresholds from recognition costs cite it when the event space is the positive reals under multiplication. The implementation is a one-line wrapper that applies derivedCost to the comparator component.
Claim. Let $m$ be a multiplicative recognizer equipped with comparator $C$. The induced cost is the map $F : (0,∞) → ℝ$ defined by $F(r) := C(r,1)$.
background
A multiplicative recognizer pairs a geometric recognizer onto positive reals with a continuous comparison operator that satisfies the four Aristotelian laws plus scale invariance. The derivedCost construction extracts a function on positive ratios by fixing the second argument at the multiplicative identity 1, which is well-defined precisely because of scale invariance.
proof idea
The definition is a one-line wrapper that applies derivedCost to the comparator field of the multiplicative recognizer.
why it matters
This cost supplies the functional that appears in the cost-rate Euler-Lagrange theorems and in acoustic derivations such as pitch JND fractions and speech intelligibility certificates. It realizes the honest conditional form of (L4) composition consistency for multiplicative event spaces, converting the abstract RecognizerComposition hypothesis into a derived theorem once the carrier is restricted to positive reals with a law-of-logic comparator. The construction therefore bridges the gap between the general recognizer framework and concrete applications in action principles and J-cost geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.