Physics Measurement Theory From Rs

Measurement levels in RS

Measurement theory, as developed by psychologist Stanley Smith Stevens in 1946, sorts the ways numbers can represent properties into four levels. Nominal measurement labels things without order, like jersey numbers. Ordinal measurement ranks them, like race positions, without saying how far apart they are. Interval measurement adds equal spacing, so the difference between 10 and 20 degrees means the same as between 30 and 40, but zero is arbitrary. Ratio measurement adds a true zero, so twice the number means twice the property, as with length or mass.

Recognition Science, a framework that derives physical structure from the cost of recognition events, extends this scheme. Its central object is the cost, a measure of how far a recognition deviates from perfect agreement. The framework proves that this cost function, written J(r), behaves as a ratio-scale measurement: J(1) = 0 gives an absolute zero of deviation, and J(r) is positive whenever r differs from 1. That zero is not arbitrary, which is why the framework classifies J-cost as a fifth level, absolute measurement, beyond Stevens' four.

The machine-checked library of formal theorems backing this framework defines the five levels as an inductive type and proves, by direct computation, that there are exactly five of them. The theorem measurementLevelCount establishes that the cardinality of the set {nominal, ordinal, interval, ratio, absolute} is 5. A certificate structure packages this proof, and a definition instantiates it. The entire module compiles with zero axioms and zero unresolved proofs, meaning the claim rests entirely on the kernel's standard postulates.

What this establishes in plain language is that the framework's cost function is not a loose metaphor but a precisely typed measurement. It occupies a well-defined place in the classical taxonomy, and the count of levels is a proved fact, not a convention. The practical consequence: when the framework speaks of recognition deviation as a quantity, it is claiming the same kind of measurability that physics claims for length or mass, with a true zero and a meaningful scale.

theorem measurementLevelCount : Fintype.card MeasurementLevel = 5 := by decide

theorem measurementLevelCount : Fintype.card MeasurementLevel = 5 := by decide

def measurementTheoryCert : MeasurementTheoryCert where
  five_levels := measurementLevelCount

What this page does not claim

The module does not prove that J-cost is the unique cost function; that is a separate theorem. The module does not derive any numerical values for physical constants. The module does not claim that Stevens' four levels are wrong, only that RS adds a fifth.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/MeasurementTheoryFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: