CostUnit
plain-language theorem explainer
CostUnit introduces the inductive type that tags cost quantities in the RS-native measurement system. Researchers constructing ledger observables or protocol-based measurements in Recognition Science would reference it to ensure type-safe cost dimensions. The declaration is a bare inductive definition with no constructors, serving as a dimension placeholder that enables the downstream Cost abbreviation.
Claim. CostUnit is the inductive type serving as the dimension for cost quantities, so that costs are formed as Quantity CostUnit in the Recognition Science native measurement scaffold.
background
The RS-Native Measurement Framework (Core) supplies a Lean-first scaffold for Recognition Science observables built from ticks, voxels, coherence, and action with base time unit τ₀ = 1. SI or CODATA values remain optional external calibration; every measurement must carry an explicit protocol. CostUnit belongs to this core layer and is used to form ledger-style cost observables without hidden arbitrary choices.
proof idea
The declaration is a direct inductive definition of CostUnit as a bare Type with no constructors or data, functioning as a unit tag for the Quantity construction.
why it matters
CostUnit supplies the dimension for the abbrev Cost := Quantity CostUnit, which downstream measurement constructions rely on to keep protocols explicit. It directly supports the module's design goal of RS-native core theory (ticks/voxels/coh/act + ledger observables) while leaving SI calibration outside the core, consistent with the eight-tick octave and phi-ladder structure of the broader Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.