Qualia
plain-language theorem explainer
Qualia denotes a real number equipped with the qualia semantic label. Researchers modeling consciousness as strain in Recognition Science cite this abbreviation to supply the typed observable for the qualia domain instance. The declaration is a direct one-line abbreviation that instantiates the generic Quantity structure over the empty inductive QualiaUnit tag.
Claim. A qualia is a real number $q$ carrying the qualia semantic unit label, written $q :$ Quantity with unit QualiaUnit, where Quantity supplies the real value together with addition, subtraction, and coercion to the reals.
background
In the RS-native measurement framework the core module supplies typed observables built from real numbers tagged by semantic units. Quantity is the structure that packages a real value with a unit label, providing the algebraic operations and coercion while keeping the label distinct. QualiaUnit is the empty inductive type that functions solely as the semantic tag for subjective-experience observables. The module keeps all definitions inside the RS-native setting with base tick equal to one and defers any SI calibration to external files.
proof idea
The declaration is a direct one-line abbreviation that applies the Quantity structure to the QualiaUnit inductive type.
why it matters
This abbreviation supplies the typed observable required by the qualia domain instance, where the cost embedding identifies J-cost directly with qualia strain. It is used by HardProblemDissolution to assert that qualia are identical to strain rather than caused by it, and appears in logic embeddings, determinism constraints, and vantage-category definitions. The construction supports the Recognition framework's treatment of qualia as phase-mismatch strain inside the recognition algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.