measurementLevelCount
plain-language theorem explainer
The theorem states that the finite type of measurement levels in Recognition Science comprises exactly five elements. Researchers formalizing measurement scales within the RS framework cite it to fix the configuration dimension at five. The proof is a one-line decision procedure that computes the cardinality from the derived Fintype instance on the inductive definition.
Claim. The set of canonical measurement scales has cardinality five: $ |M| = 5 $, where $M$ consists of the nominal, ordinal, interval, ratio, and absolute scales.
background
The module Measurement Theory from RS defines five canonical measurement types that equal configDim D = 5. J-cost functions as a ratio-scale measurement of recognition deviation, with J(1) = 0 marking absolute zero of deviation and J(r) > 0 for r ≠ 1. Stevens' levels supply the first four scales while RS adds the absolute scale as the fifth, identified with J-cost itself.
proof idea
The proof is a one-line wrapper that applies the decide tactic. It relies on the Fintype instance automatically derived from the inductive definition of MeasurementLevel, which enumerates the five constructors and supplies the required DecidableEq and cardinality computation.
why it matters
This result supplies the five_levels field inside the measurementTheoryCert definition, completing the certification of measurement theory in the RS setting. It directly implements the module statement that five levels equal configDim D = 5 and extends the classical scales by tying the absolute level to J-cost. No explicit connection to the forcing chain T0-T8 or the Recognition Composition Law appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.