Contingent
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert existence of any contingent property.
- Does not define the types Config or ConfigProp.
- Does not relate contingency to the phi-ladder or mass formula.
- Does not prove invariance under the Recognition Composition Law.
formal statement (Lean)
101def Contingent (p : ConfigProp) (c : Config) : Prop :=
proof body
Definition body.
102 p (Actualize c) ∧ Degenerate c ∧
103 ∃ y ∈ Possibility c, J y.value = J (Actualize c).value ∧ ¬p y
104
105/-- **DETERMINED**: A property that could not have been otherwise.
106
107 p is determined at c if all cost-minimal successors satisfy p. -/