MeasurementTheoryCert
plain-language theorem explainer
The certificate structure asserts that the set of measurement levels has cardinality five, matching the five canonical scales in Recognition Science. Researchers deriving measurement theory from the framework cite it to fix the dimensionality of scales at five before building higher-level results. It is realized as a structure definition whose single field holds the cardinality equality, satisfied directly by the inductive enumeration of the levels.
Claim. The structure certifies that the cardinality of the set of measurement levels equals five, where the levels are the nominal, ordinal, interval, ratio, and absolute scales.
background
The module derives measurement theory from Recognition Science by identifying J-cost as a ratio-scale measure of recognition deviation, with J(1) = 0 serving as the absolute zero. Stevens' four scales are extended by the absolute scale given by J-cost itself, yielding exactly five types. The local setting states that these five types equal configDim D = 5, with Lean encoding them as an inductive type whose finite cardinality is asserted by the certificate.
proof idea
The declaration is a structure definition. Its single field is discharged by the cardinality of the inductive type that enumerates the five measurement levels.
why it matters
This definition is instantiated by the downstream measurementTheoryCert construction in the same module. It supplies the five-dimensional measurement space required by the Recognition Science framework, consistent with the forcing chain that derives D = 3 spatial dimensions and the phi-ladder for mass scales. It touches the open question of how the absolute scale emerges from J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.