pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

Cost

show as:
view Lean formalization →

Cost supplies the typed carrier for real-valued cost observables inside the RS-native measurement system. Acoustics and action-principle authors cite it when they instantiate J-cost functions or hearing-loss penalties. The declaration is a one-line abbreviation that delegates all algebraic structure (zero, addition, coercion to ℝ) to the Quantity structure.

claimLet $Cost$ denote the type of real-valued quantities equipped with the semantic label $CostUnit$.

background

The RS-Native Measurement Framework represents every observable as a real number tagged with a unit type. Quantity U is the structure that packages a real val together with the unit U and supplies the zero, addition, subtraction, and coercion-to-ℝ instances. CostUnit is an empty inductive type whose sole purpose is to serve as the semantic tag for cost quantities.

proof idea

This is a direct abbreviation that instantiates Quantity at the CostUnit inductive type. No lemmas or tactics are invoked; the declaration simply re-exports the real carrier and its algebraic instances.

why it matters in Recognition Science

Cost is the carrier used by forty downstream declarations, among them srCost, hearingLossPenalty_nonneg, and costRateEL_const_one. It anchors the J-cost function (derived from the Recognition Composition Law and T5 J-uniqueness) inside the typed measurement system, guaranteeing that nonnegativity and reciprocal symmetry are inherited automatically. The definition therefore closes the interface between the abstract forcing chain and concrete observables such as speech-recognition costs.

scope and limits

formal statement (Lean)

 204abbrev Cost := Quantity CostUnit

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.