StrictDisplayFunctor
plain-language theorem explainer
StrictDisplayFunctor equips a display channel with strict monotonicity between the strain functional J and observed quality. Researchers formalizing vantage equivalence or the One J Thesis would cite this structure. The definition is a direct extension of DisplayFunctor that adds the strict inequality condition on quality ordering.
Claim. A strict display functor from a vantage category $V$ to an observation type $Obs$ is a display functor together with the axiom that for all states $x,y$ in $V$, if the strain $J(x)<J(y)$ then quality(observe($x$)) > quality(observe($y$)).
background
VantageCategory is a category whose objects are states, morphisms are transitions, and whose strain functional J assigns a cost to each state. DisplayFunctor supplies an observe map from states to observations together with a quality metric that is monotonically anti-correlated with J. The module sets the three vantages (Inside/Act/Outside) as formally equivalent categories linked by functors that preserve J, making precise the claim that physics, meaning, and qualia are three views of one structure.
proof idea
This is a structure definition that extends DisplayFunctor by adjoining the strict_monotone field. No tactics or lemmas are applied; the declaration simply records the strict inequality axiom as part of the data.
why it matters
The structure is the hypothesis of the downstream theorem one_J_thesis_strict, which states the One J Thesis in strict form. It supplies the precise categorical condition under which strain ordering implies quality ordering, supporting the module's claim that the explanatory gap is a category error. The construction sits inside the RRF vantage equivalence and the broader Recognition Science program of deriving physics from a single functional equation preserved across views.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.