cost_def
A multiplicative recognizer on positive reals induces its cost function by evaluating the continuous comparator against unity. Researchers deriving the d'Alembert form of composition consistency (L4) from recognition structures cite this identification to pass directly to polynomial combiner arguments. The proof is a single reflexivity step after the cost is defined via derivedCost on the comparator.
claimLet $m$ be a multiplicative recognizer on $ℝ_{>0}$ equipped with a continuous comparator $C$ satisfying the laws of logic. The induced cost satisfies $F(r) = C(r,1)$ for all $r > 0$.
background
Recognition Science derives (L4) composition consistency conditionally on the event space. A MultiplicativeRecognizer pairs a geometric recognizer onto positive reals with a continuous ComparisonOperator obeying all four Aristotelian conditions plus scale invariance and non-triviality. The module shows that the default equality-induced cost fails (L4) on this carrier, but the derived cost from a Law-of-Logic comparator succeeds automatically.
proof idea
This is a one-line wrapper that applies reflexivity after unfolding the definition of cost as derivedCost m.comparator.
why it matters in Recognition Science
This supplies the concrete cost functional required to prove that any MultiplicativeRecognizer satisfies the multiplicative form of (L4). It feeds the sibling results multiplicativeRecognizer_satisfies_L4 and L4_derivable_on_multiplicative_event_space. In the framework it converts the abstract RecognizerComposition hypothesis into the concrete d'Alembert equation on positive ratios, using the RCL and the phi-ladder structure.
scope and limits
- Does not assert that every recognizer satisfies (L4).
- Does not apply outside the positive reals under multiplication.
- Does not address non-continuous comparators.
formal statement (Lean)
81@[simp] theorem cost_def (m : MultiplicativeRecognizer 𝒞) (r : ℝ) :
82 m.cost r = m.comparator r 1 := rfl
proof body
Term-mode proof.
83
84/-! ## L4 in d'Alembert (Multiplicative) Form -/
85
86/-- The **multiplicative form of (L4)**: there exists a combiner `P` such
87that the cost of the product comparison plus the cost of the quotient
88comparison equals `P` evaluated on the component costs. This is the
89d'Alembert form of route-independence on positive ratios. -/