CostUnit
plain-language theorem explainer
CostUnit is the inductive base type for cost quantities inside the RS-native measurement scaffold. It is referenced by any construction of ledger observables or protocol-wrapped measurements that need an explicit dimension for cost. The declaration is a minimal inductive type with no constructors or cases.
Claim. CostUnit is the inductive type that serves as the dimension for cost in the Recognition Science native measurement system, where core observables are built from ticks, voxels, coherence and action with $τ_0=1$.
background
The module establishes a Lean-first measurement scaffold for Recognition Science in which every observable carries an explicit protocol and falsifiers. Core theory remains RS-native (ticks/voxels/coh/act) while SI/CODATA calibration lives outside. CostUnit supplies the dimension type that lets Quantity wrap cost without importing external units.
proof idea
Bare inductive declaration of a Type with no constructors or cases; no lemmas or tactics are applied.
why it matters
CostUnit is the immediate prerequisite for the abbrev Cost := Quantity CostUnit, which downstream measurement catalog entries rely on to keep cost observables protocol-explicit. It directly supports the module goal of making arbitrary choices (windowing, coarse-graining) visible rather than hidden.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.