determined_necessary_for_minimal
plain-language theorem explainer
Determined properties hold for every possibility whose J-cost matches the actualized configuration. Modal physicists formalizing necessity in Recognition Science cite this result when showing that minimal-cost outcomes are the only ones satisfying determined predicates. The proof is a direct one-line term application of the hypothesis that encodes the definition of Determined.
Claim. If property $p$ is determined at configuration $c$, then every possibility $y$ of $c$ satisfying $J(y.value) = J( (Actualize c).value )$ obeys $p(y)$.
background
In the Modal.Actualization module, which imports Possibility, a Config carries a ConfigProp that may be classified as Determined, Contingent, or Degenerate. The predicate Determined p c is defined to mean that p holds for all y in Possibility c whenever the J-cost of y equals the J-cost of the actualized successor. J is the recognition cost function supplied by upstream cost definitions in ObserverForcing and MultiplicativeRecognizerL4; Actualize selects the minimal-cost outcome among possibilities.
proof idea
The proof is a one-line term wrapper that applies the hypothesis hd directly; no further lemmas or tactics are invoked.
why it matters
The declaration closes the interface between the Determined predicate and cost equivalence inside the actualization framework. It supports the surrounding ActualizationPrinciple and PathAction constructions that follow in the same module, and it aligns with the Recognition Science forcing chain at the step where minimal J-cost selects realized outcomes (T5 J-uniqueness and the phi-ladder). No downstream uses are recorded yet, leaving open how this necessity will be invoked in later modal or Born-rule arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.