ActualizationPrinciple
plain-language theorem explainer
The ActualizationPrinciple structure packages a current configuration with a successor that belongs to its possibility set and attains the global minimum J-cost within that set. Modal dynamics in Recognition Science cite this record as the explicit witness for cost-driven state selection. The declaration is a bare structure definition whose four fields directly encode the argmin condition with no lemmas or tactics required.
Claim. An actualization principle for a configuration $c$ consists of a successor configuration $s$ together with a proof that $s$ lies in the possibility set $P(c)$ and that $J(s) = J(s.value)$ is minimal among all $y$ in $P(c)$, where $J$ denotes the recognition cost function.
background
In the modal layer, configurations are drawn from the ILG Config type. The possibility set Possibility c collects admissible successor states, while the cost function J is the recognition cost: either derivedCost from a MultiplicativeRecognizer comparator or the Jcost of a recognition event. The structure therefore implements the selection rule that the universe evolves by choosing cost-minimizing futures from the current possibility set.
proof idea
The declaration is a structure definition with four fields: current and successor of type Config, the membership predicate in_possibility, and the universal quantification minimizes_cost. No lemmas are applied and no tactics are used; the structure simply packages the data and the two propositions.
why it matters
This definition supplies the witness type for has_actualization, which asserts that every configuration admits at least one actualization. It directly encodes the core dynamical rule of Recognition Science: selection of argmin J(y) from P(c). In the forcing chain it realizes the transition from possibility to actuality, consistent with the eight-tick octave and the phi-ladder mass formulas. The doc-comment notes that uniqueness yields determinism while degeneracy requires further structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.