MeasurementLevel
Recognition Science models measurement via five levels where the absolute level corresponds to direct J-cost evaluation with J(1) = 0. Researchers formalizing Stevens' scales augmented by RS would cite this enumeration to fix configDim D = 5. The declaration is a direct inductive definition that derives decidability and finiteness instances.
claimThe measurement levels are the inductive type whose constructors are nominal, ordinal, interval, ratio, and absolute.
background
Recognition Science derives all measurement from the J-cost functional J(r) with J(1) = 0 as absolute zero deviation and J(r) > 0 for r ≠ 1. Stevens' classical hierarchy supplies nominal (1), ordinal (2), interval (3), and ratio (4) scales; RS adds absolute as the fifth level that measures J-cost directly. The module sets these five types equal to configDim D = 5. The upstream interval definition supplies the spacetime metric background used elsewhere in the unification layer.
proof idea
The declaration is a direct inductive definition that lists the five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances.
why it matters in Recognition Science
This definition supplies the type for the measurementLevelCount theorem establishing Fintype.card = 5 and for the MeasurementTheoryCert structure. It realizes the framework step that five measurement types equal configDim D = 5, connecting Stevens' scales to the absolute J-cost scale. No open questions or scaffolding are touched.
scope and limits
- Does not assign numerical values or orderings to the levels.
- Does not connect levels to explicit J-cost formulas.
- Does not derive theorems about measurement operations or conversions.
formal statement (Lean)
22inductive MeasurementLevel where
23 | nominal | ordinal | interval | ratio | absolute
24 deriving DecidableEq, Repr, BEq, Fintype
25