A
plain-language theorem explainer
The actualization operator selects for each configuration c the element of minimal J-cost inside the possibility set generated by c. Modal dynamics researchers cite it to separate what could occur from what does occur under the Recognition Science forcing chain. The declaration is a direct one-line alias to the imported Actualize function.
Claim. Let $A : Config → Config$ satisfy $A(c) = argmin_{y ∈ P(c)} J(y)$, where $P$ is the possibility operator and $J$ is the cost functional obeying $J(x) = (x + x^{-1})/2 - 1$.
background
Configurations carry the ILG structure with fields upsilonStar, eps_r, eps_v, eps_t, eps_a. The cost functional J is fixed by T5 uniqueness as $J(x) = (x + x^{-1})/2 - 1$ (equivalently cosh(log x) - 1). The possibility operator P supplies the admissible successor set for any c. The active-edge count per tick is fixed at 1 by the integration-gap identity φ^(A - gap) · φ^gap = φ at D = 3.
proof idea
One-line definition that aliases the Actualize function imported from the Possibility module. The attached comment records well-definedness; no tactics or further lemmas are invoked.
why it matters
Downstream results on energy conservation under time translation, Christoffel symbols of the Hessian metric 1/x³, J-action convexity, and Noether space/time shifts all invoke this operator. It supplies the selection step that completes the modal pair (P, A) and connects to T5 J-uniqueness and T6 self-similar fixed point. The definition closes the modal-dynamics interface used by forty later declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.