QualiaUnit
plain-language theorem explainer
QualiaUnit defines an inductive type that acts as the base unit for qualia quantities inside the RS-native measurement scaffold. Measurement researchers cite it when building protocol-explicit observables from ledger data with τ₀ = 1. The declaration is a direct inductive type introduction carrying no constructors or proof content.
Claim. QualiaUnit is an inductive type in the universe of types that serves as the dimensional unit for qualia quantities in the Recognition Science measurement framework.
background
The module supplies a Lean-first scaffold for Recognition Science measurements. Core theory remains RS-native with ticks, voxels, coherence, action and ledger observables fixed at τ₀ = 1; SI/CODATA values appear only as optional external calibration. QualiaUnit supplies the unmarked base type from which quantities are later formed.
proof idea
The declaration is a bare inductive type definition with no constructors listed and no proof obligations.
why it matters
QualiaUnit is the immediate predecessor of the abbrev Qualia := Quantity QualiaUnit. It anchors the explicit-protocol measurement layer that the module positions between raw RS observables and downstream catalog entries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.