IndisputableMonolith.Physics.MeasurementTheoryFromRS

   1import Mathlib
   2
   3/-!
   4# Measurement Theory from RS — Foundation
   5
   6Five canonical measurement types (nominal, ordinal, interval,
   7ratio, absolute) = configDim D = 5.
   8
   9In RS: J-cost is a ratio-scale measurement of recognition deviation.
  10J(1) = 0 (absolute zero of deviation), J(r) > 0 for r ≠ 1.
  11
  12Stevens' levels: nominal (1), ordinal (2), interval (3), ratio (4).
  13RS adds: absolute = the 5th scale (J-cost itself).
  14
  15Lean: 5 measurement types.
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith.Physics.MeasurementTheoryFromRS
  21
  22inductive MeasurementLevel where
  23  | nominal | ordinal | interval | ratio | absolute
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem measurementLevelCount : Fintype.card MeasurementLevel = 5 := by decide
  27
  28structure MeasurementTheoryCert where
  29  five_levels : Fintype.card MeasurementLevel = 5
  30
  31def measurementTheoryCert : MeasurementTheoryCert where
  32  five_levels := measurementLevelCount
  33
  34end IndisputableMonolith.Physics.MeasurementTheoryFromRS
  35