Determined
plain-language theorem explainer
A property p of configurations is determined at c when it holds for every possible successor y whose J-cost equals the J-cost of the actualized state. Modal modelers in Recognition Science cite this definition to mark properties fixed by cost minimization rather than contingency. The definition is a direct predicate that isolates the minimal-cost slice of the possibility set through J-value equality.
Claim. A property $p$ of configurations is determined at configuration $c$ when every successor $y$ in the possibility set of $c$ satisfying $J(y) = J(A(c))$ also satisfies $p(y)$, where $A$ denotes the actualization operator that selects the J-cost minimizer.
background
In the modal layer, a configuration is a point in recognition state space carrying a positive real value and a time coordinate in ticks. The possibility operator generates the set of potential successors while actualization selects the unique J-minimizer among them; J-cost is the non-negative recognition cost induced by the multiplicative comparator on positive ratios. ConfigProp is the type of predicates on configurations. This definition appears in the Actualization module, which develops the distinction between what could happen and what does happen under cost selection.
proof idea
This is a definition whose body directly encodes the required universal quantification. It identifies the cost-minimal slice by testing equality of J values against the actualized configuration and requires p to hold on that slice.
why it matters
The definition is invoked by the theorem determined_necessary_for_minimal to establish necessity among cost-equivalents. It supports downstream results including backpropagation completeness under isolation invariants and amplitude bounds for gravity parameters. In the Recognition Science framework it realizes the actualization principle by anchoring modal necessity to J-minimization, consistent with the forcing chain steps that derive J-uniqueness and the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.