Cost
plain-language theorem explainer
Cost is defined as the type of real numbers carrying the CostUnit semantic label. Acoustics and action researchers cite it when tagging J-cost observables such as speech-recognition penalties or Euler-Lagrange rates. The declaration is a direct type alias with no further computational content.
Claim. Cost denotes the type of real-valued quantities equipped with the semantic label CostUnit.
background
The module supplies an RS-native measurement scaffold in which every observable is a real number tagged with an explicit unit or semantic label; SI calibration lives outside the core. Quantity is the structure carrying a single field val : ℝ together with the expected additive group instances. CostUnit is the empty inductive marker that distinguishes cost-tagged quantities from other semantic labels such as time or length.
proof idea
This declaration is a one-line type abbreviation that equates Cost to Quantity CostUnit.
why it matters
Cost supplies the semantic tag used by forty downstream declarations, including srCost, hearingLossPenalty_nonneg, and costRateEL_const_one. It anchors the measurement layer of the Recognition framework so that J-cost observables remain distinguishable from other ledger quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.