has_actualization
plain-language theorem explainer
The definition has_actualization asserts that a configuration c admits an ActualizationPrinciple witness with matching current state. Modal logicians in Recognition Science cite this predicate when establishing that every state can evolve toward a cost-minimizing successor. It is realized directly as an existential quantification over the ActualizationPrinciple structure.
Claim. For a configuration $c$, the proposition that there exists an actualization principle $ap$ such that the current configuration of $ap$ equals $c$.
background
In the Modal.Actualization module, a configuration is a point in recognition state space with a positive real value and time coordinate in ticks. The ActualizationPrinciple structure encodes the dynamical rule that the universe selects cost-minimizing futures: given current state $c$, among all $y$ in the possibility set $P(c)$, select the argmin of the J-cost function.
proof idea
The definition is a direct existential statement over the ActualizationPrinciple structure whose current field equals the input configuration $c$. It functions as a one-line wrapper with no lemmas or tactics applied.
why it matters
This definition supports the theorem every_config_actualizes, which states that every configuration has an actualization toward identity. It operationalizes the selection rule argmin J(y) in the modal layer, connecting to the J-cost minimum at the identity event where state equals 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.