QualiaUnit
plain-language theorem explainer
QualiaUnit introduces an inductive type as the base for qualia quantities inside the RS-native measurement scaffold. It is cited by any construction of Quantity instances that carry explicit protocols and falsifiers. The declaration is a bare inductive type definition with no constructors or attached lemmas.
Claim. An inductive type of sort Type is declared to serve as the unit for qualia quantities.
background
The module supplies a Lean-first scaffold for Recognition Science measurements. Core theory stays RS-native with ticks, voxels, coherence and action at τ₀ = 1; SI/CODATA calibration remains external. Every measurement must carry an explicit protocol so that windowing and basis choices cannot be hidden. The file is kept small and dependency-light, with concrete observables deferred to Catalog modules.
proof idea
The declaration is a direct inductive definition that establishes the type with no constructors or further structure.
why it matters
The type supplies the unit for the downstream abbrev Qualia := Quantity QualiaUnit, anchoring the measurement framework's emphasis on explicit protocols. It supports the design goal of keeping core theory RS-native while leaving calibration outside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.