every_config_actualizes
plain-language theorem explainer
Every configuration admits an actualization to the identity configuration after eight time steps. Modal physicists working in Recognition Science cite this to guarantee that cost-minimizing selection from possibilities is always defined. The proof constructs an explicit witness for the actualization predicate by shifting to the identity configuration and verifying minimality via the normalization J(1)=0 together with non-negativity of J.
Claim. For every configuration $c$, there exists an actualization of $c$ consisting of a successor at time shifted forward by eight steps that belongs to the possibility set and achieves the global minimum of the J-cost function.
background
In the Modal.Actualization module, configurations are states in the modal space from which the actualization operator selects a successor by minimizing J-cost. The J-cost is the derived cost function on positive ratios induced by a multiplicative recognizer, satisfying J(1)=0 by the normalization result. Upstream results establish that the cost of any recognition event is non-negative and that the multiplicative identity carries zero cost. This layer sits above observer forcing and phi-forcing, where actualization resolves possibilities into realized paths.
proof idea
The tactic proof constructs the witness structure directly. It sets the successor to the identity configuration advanced by eight ticks, invokes the lemma that the identity configuration is always possible, and establishes cost minimality by simplification using the zero-cost normalization at unity followed by an appeal to non-negativity of J.
why it matters
This theorem establishes universal existence of actualizations and feeds directly into the actualization status definition. It realizes the ActualizationPrinciple by ensuring every configuration possesses a minimal-cost continuation, consistent with the eight-tick octave in the forcing chain. It leaves open how degeneracy among multiple minimal paths originates contingency, as flagged in the module's degeneracy section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.