adjoint_from_cost_monotonic
plain-language theorem explainer
Cost-monotonic properties transfer from any possible configuration y to the actualized A(c) whenever J-cost strictly decreases. Modal actualization arguments in Recognition Science cite this to guarantee inheritance under the minimization operator. The proof is a direct one-line application of the CostMonotonic definition to the pair y and A(c).
Claim. Let $p$ be a cost-monotonic property of configurations. For configuration $c$ and $y$ in the possibility set of $c$ with $p(y)$ holding, if $J(y.value) > J((A(c)).value)$ and $(A(c)).value > 0$, then $p(A(c))$ holds.
background
The module Modal.Actualization introduces the actualization operator A as the cost-minimizing element in the possibility set: A(c) = argmin_{y in Possibility(c)} J(y). CostMonotonic(p) is the hypothesis that p propagates down the J-cost gradient: p(y) and J(y.value) > J(y'.value) with y'.value > 0 imply p(y'). J-cost itself is supplied by upstream definitions in MultiplicativeRecognizerL4 and ObserverForcing, where cost(e) = Jcost(e.state) for recognition events. The local setting pairs this with the dual Possibility operator to formalize the modal distinction between what could occur and what does occur.
proof idea
One-line wrapper that applies the CostMonotonic predicate directly: substitute y and A(c) into the universal quantification, using the supplied hp, the cost inequality, and the positivity guard hA_pos.
why it matters
This result secures the adjoint direction for cost-monotonic properties inside the actualization framework, feeding the module's ActualizationPrinciple and related statements on determined and contingent configurations. It aligns with the Recognition Science forcing chain by ensuring that the J-minimizer inherits monotonic structure, consistent with J-uniqueness (T5) and the phi-ladder mass formulas. No downstream uses are recorded yet, leaving open whether the same transfer extends to non-monotonic properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.