actualize_decreases_cost
plain-language theorem explainer
Actualization selects the J-minimizing successor from a configuration whose value differs from one. Modal researchers in Recognition Science cite the result to confirm that the selection step strictly lowers cost. The proof is a term-mode reduction that unfolds the actualize definition then applies the positivity lemma for J.
Claim. Let $c$ be a configuration with value $v > 0$ and $v ≠ 1$. Then $J(Actualize(c).value) < J(v)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
In the Modal.Possibility module a configuration is a point in recognition state space given by a positive real value, a positivity witness, a time coordinate in ticks, and a log-bound constraint. The cost function J is the unique function satisfying d'Alembert normalization and calibration, written explicitly as half the sum of its argument and reciprocal minus one. Actualize is defined to return the identity configuration at time advanced by eight ticks. The result rests on the upstream theorem that J(1) equals zero.
proof idea
The term proof first simplifies the definitions of Actualize and identity_config together with the fact that J(1) = 0. This reduces the left-hand side to zero. The remaining inequality is discharged exactly by the positivity lemma J_pos_of_ne_one applied to the configuration's positivity witness and the hypothesis that the value differs from one.
why it matters
The theorem is invoked directly by A_toward_identity in the Actualization module, which records that the operator A drives configurations toward the identity. It supplies the modal step that actualization decreases cost, consistent with the J-minimizer property from T5 in the forcing chain. The result closes one link in the grammar of possibility while leaving open the question of global convergence under iterated actualization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.