DisplayFunctor
plain-language theorem explainer
DisplayFunctor equips a VantageCategory with an observation map from states to an external type together with a real-valued quality metric that reverses the ordering induced by the strain functional J. Researchers formalizing vantage equivalence in Recognition Science cite this structure when building observation channels that preserve cost orderings. The declaration is a direct structure definition introducing the map, the metric, and the single monotonicity field.
Claim. Let $V$ be a vantage category with state space $S$ and strain functional $J$. A display functor to an observation type $O$ consists of a function $o: S → O$, a quality map $q: O → ℝ$, and the property that $J(x) ≤ J(y)$ implies $q(o(x)) ≥ q(o(y))$ for all states $x,y$.
background
The module shows that the three vantages are categorically equivalent via functors that preserve the strain functional J, making precise the claim that physics, meaning, and qualia are three views of one structure. A VantageCategory is defined as a category whose objects are states, whose morphisms are transitions, and whose states carry costs under the strain functional J. Upstream results supply concrete realizations of J-cost, including the inflaton potential $V(φ_inf) = J(1 + φ_inf)$ and the vertex count $V(D) = 2^D$ on the recognition manifold.
proof idea
This is a structure definition that directly introduces the three fields: the observation map, the quality function on observations, and the monotonicity constraint relating quality to strain ordering. No lemmas are applied; the definition stands as the primitive interface.
why it matters
The structure is the parent for ChannelCoherence, which requires indexed families of channels to agree on quality orderings, and for the weak One J Thesis that derives quality ordering directly from strain ordering. It supplies the categorical step supporting the vantage equivalence claim in the module doc-comment. It touches the open question of constructing explicit functors between the Inside, Act, and Outside vantages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.