Contingent
plain-language theorem explainer
A property p is contingent at configuration c when p holds of the actualized successor A(c), c is degenerate, and some equal-J-cost possibility y in Possibility c violates p. Modal physicists or logicians working inside Recognition Science cite the definition to separate contingent from determined features under the Actualize operator. The definition is assembled directly as the conjunction of the three clauses supplied in its documentation.
Claim. A property $p$ is contingent at configuration $c$ if $p(A(c))$ holds, $c$ is degenerate, and there exists $y$ in the possibility set of $c$ such that $J(y) = J(A(c))$ and $p$ fails at $y$.
background
The Actualization operator A maps a configuration to its cost-minimizing successor: A(c) equals the argmin of J over the possibility set P(c). Possibility c supplies the set of admissible successors while J records the recognition cost of each. Degenerate c indicates that the minimum is attained by more than one element of that set. The module Modal.Actualization sits inside the modal layer that distinguishes what must occur from what could occur once the forcing chain has fixed the actual path.
proof idea
One-line definition that directly encodes the three conditions stated in the doc-comment: satisfaction of p under Actualize, degeneracy of c, and existence of an equal-J-cost alternative violating p.
why it matters
The definition supplies the modal counterpart to the Determined sibling inside the same module, allowing the framework to express properties that could have been otherwise once the eight-tick octave and D=3 geometry are fixed. It feeds the ActualizationPrinciple and has_actualization declarations listed among the siblings, completing the basic modal vocabulary required for the Recognition Composition Law to act on both actual and possible branches.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.