H_adjoint_non_minimal
plain-language theorem explainer
Cost-monotonic properties transfer from any witness in the possibility set of c to the actualized configuration A(c) whenever the witness carries strictly positive cost. Modal logicians in Recognition Science cite the result to obtain conditional adjointness between possibility and actualization operators. The proof derives the strict cost inequality from non-negativity of J together with the given nonzero assumption, then invokes the monotonicity hypothesis directly.
Claim. Let $p$ be a cost-monotonic property on configurations. Suppose $c$ is a configuration, $y$ lies in the possibility set of $c$, $p(y)$ holds, $J(y)$ is nonzero, and the actualized configuration $A(c)$ has positive value. Then $p(A(c))$ holds.
background
In the Modal.Actualization module the actualization operator A sends a configuration c to the cost-minimizing element of its possibility set. A property p is cost-monotonic when p(y) and J(y) > J(y') with y'.value > 0 together imply p(y'). The theorem treats the non-minimal case in which the witness y has positive cost, so that adjointness requires the monotonicity assumption. Upstream, J_at_one states that the multiplicative identity carries zero cost, which is used to identify the cost of A(c).
proof idea
The proof first obtains J(y.value) > 0 by case analysis on lt_or_eq_of_le applied to J_nonneg y.pos, discarding the zero case via the nonzero hypothesis. It then shows J((A c).value) = 0 by simplification with the definitions of A and Actualize together with J_at_one. The resulting strict inequality J(y.value) > J((A c).value) is fed directly into the cost-monotonicity hypothesis to conclude p(A c).
why it matters
The declaration supplies the non-minimal half of the adjointness relation between possibility and actualization that the module documentation identifies as the mathematical core of RS modal logic. It therefore supports the broader ActualizationPrinciple and has_actualization results by showing how cost-monotonic properties descend the cost gradient. The result aligns with the forcing chain (T5 uniqueness, T6 fixed-point phi) and the recognition composition law by enforcing cost ordering on modal operators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.