possibility_actualization_adjoint_minimal
plain-language theorem explainer
The theorem establishes adjointness between the possibility operator and the actualization operator A for any property p, under the hypothesis that minimal-cost witnesses in the possibility set are unique. Modal logicians working in Recognition Science cite this when relating potential states to realized configurations under cost minimization. The proof is a direct biconditional construction that applies uniqueness on the forward direction after invoking J(1) = 0 and exhibits the actualized element on the reverse direction.
Claim. Let $P(c)$ be the set of possible configurations reachable from $c$, let $A(c)$ be the configuration of minimal $J$-cost in $P(c)$, and let $p$ be any predicate on configurations. If every $y$ in $P(c)$ with $J(y) = J(A(c))$ equals $A(c)$, then there exists $y$ in $P(c)$ such that $J(y) = J(A(c))$ and $p(y)$ holds if and only if $p(A(c))$ holds.
background
In the Modal.Actualization module the actualization operator A is defined to return the argmin of the cost function J over the possibility set P(c). The cost function J is the one induced by multiplicative recognizers and satisfies the normalization J(1) = 0. This adjointness statement forms part of the modal layer that sits above the forcing chain and the Recognition Composition Law.
proof idea
The tactic proof opens the biconditional with constructor. The forward direction uses J_at_one to obtain J(y) = 0, applies the uniqueness hypothesis to equate y with A(c), and substitutes into p. The reverse direction directly supplies A(c) together with the fact that the identity configuration is always possible.
why it matters
This supplies the core adjointness between possibility and actualization that underpins modal reasoning in Recognition Science. It supports the ActualizationPrinciple and related modal definitions in the same module. The result encodes how predicates true of the realized configuration coincide with those true of its minimal-cost possibility, consistent with the self-similar fixed point and cost minimization steps in the T5-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.