A_well_defined
plain-language theorem explainer
The lemma shows that the actualization operator A, which selects the J-cost minimizer inside the possibility set P(c), always returns a configuration whose value is strictly positive. Modal physicists applying Recognition Science to configuration dynamics would cite it to guarantee that actualized states remain inside the valid domain. The proof is a one-line wrapper that invokes the actualize_valid lemma from the Possibility module.
Claim. For every configuration $c$, the actualized configuration $A(c)$ satisfies $(A(c)).value > 0$.
background
The Actualization module defines the operator A as the map sending each configuration c to the J-cost minimizer over the possibility set P(c). This operator is dual to the possibility operator P: P enumerates what could occur while A selects what does occur. The underlying Config structure, imported from Gravity.ILG, carries the parameters upsilonStar, eps_r, eps_v, eps_t, eps_a that label each recognition event. The upstream lemma actualize_valid states that actualization always produces a valid configuration, and the identity event (zero J-cost at state 1) supplies the canonical minimizer.
proof idea
The proof is a one-line wrapper that applies the actualize_valid lemma from Modal.Possibility directly to the input configuration c.
why it matters
The result secures the well-definedness of the actualization operator inside the modal layer of Recognition Science. It supports the duality between possibility and actualization that appears in the forcing chain after the J-uniqueness step (T5) and before the eight-tick octave (T7). By guaranteeing positive value, the lemma ensures that every actualized state lies above the Berry creation threshold and remains compatible with the identity event at the J-cost minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.