qualiaDomain
plain-language theorem explainer
QualiaDomain instantiates the Recognition Algebra functor for the qualia domain by supplying a record with unit state space and identity cost embedding. Researchers modeling observer strain or phase mismatch in Recognition Science cite this when building domain-specific algebras from the canonical RecAlg structure. The definition proceeds by direct record construction of the four DomainInstance fields.
Claim. The qualia domain instance is the structure whose name is Qualia (ULQ), whose state space is the unit type, whose cost embedding is the identity map on reals, and whose monotonicity condition requires that the embedding preserve the order on reals.
background
DomainInstance is the structure that turns the canonical Recognition Algebra into a concrete domain algebra; its four fields are a string name, a state type, a cost embedding map from reals to reals, and a proof that the embedding is monotone. The upstream cost definitions supply the J-cost: one from the multiplicative recognizer (derivedCost on positive ratios) and one from recognition events (Jcost of the event state). The Identity definition records that self-comparison costs zero, which is the algebraic counterpart of A = A. The local module sets up the Recognition Category with objects RecAlgObj and morphisms RecAlgHom together with the standard identity and composition operations.
proof idea
Direct record construction that supplies the four fields of DomainInstance: the name string, the Unit state type, the identity costEmbed, and the trivial monotonicity proof that any inequality is preserved under the identity map.
why it matters
This definition supplies the qualia instantiation required by the Recognition Category, directly implementing the doc-comment relation strain = phase_mismatch × J(intensity). It sits downstream of the cost functions from MultiplicativeRecognizerL4 and ObserverForcing and upstream of any future qualia-specific theorems that would apply the functor to RecAlg. The construction closes the interface for the qualia domain while leaving the concrete state space as a placeholder, consistent with the eight-tick octave and J-uniqueness landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.