pith. machine review for the scientific record. sign in
def definition def or abbrev high

A

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 254def A : Config → Config := Actualize

proof body

Definition body.

 255
 256/-- A is well-defined (always produces valid config). -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (9)

Lean names referenced from this declaration's body.