MeasurementLevel
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.