possibility_actualization_adjoint_monotonic
plain-language theorem explainer
The theorem proves adjointness between the possibility operator and actualization for cost-monotonic properties: possibility of p at c holds exactly when p holds at A(c). Modal physicists or logicians working in Recognition Science would cite it to justify propagation of properties along cost gradients. The proof uses constructor to split the biconditional, then case analysis on whether the witness has zero J-cost, reducing via J_at_one and the monotonicity hypothesis.
Claim. Let $p$ be a cost-monotonic property of configurations. For any configuration $c$, the possibility of $p$ at $c$ is equivalent to $p$ holding at the actualized configuration $A(c)$.
background
In the Modal.Actualization module the actualization operator is defined by $A(c) :=$ Actualize $c$, the cost-minimizing element of the possibility set for $c$. CostMonotonic $p$ is the hypothesis that $p$ propagates down the cost gradient: if $p(y)$ and $J(y.value) > J(y'.value)$ with $y'.value > 0$, then $p(y')$. This rests on the cost algebra fact $J(1) = 0$ from J_at_one and on the definition of possibility as existence of a witness configuration with positive value.
proof idea
The tactic proof opens with constructor to obtain the two directions of the biconditional. Forward: introduce a witness $y$ for possibility, then case on whether $J(y.value) = 0$. The zero case substitutes $y = $ identity_config via J_zero_iff_one and shows equality with $A c$. The positive case applies the CostMonotonic hypothesis directly using the strict inequality $J(y.value) > 0 = J(A c.value)$. Reverse: witness with $A c$ via identity_always_possible.
why it matters
The result supplies the adjointness of possibility and actualization under the cost-monotonicity hypothesis, a central link in the modal layer of Recognition Science. It encodes the principle that properties descend the J-cost gradient to the minimal state, consistent with the forcing chain and the definition of A as argmin. Although an accompanying module comment presents a related statement as an axiom, this theorem discharges the claim once CostMonotonic is assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.