Contingent

formal source

  98    p is contingent at c if:
  99    1. p holds for the actualized successor
 100    2. There exists a degenerate possibility where ¬p holds -/
 101def Contingent (p : ConfigProp) (c : Config) : Prop :=
 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. -/
 108def Determined (p : ConfigProp) (c : Config) : Prop :=
 109  ∀ y ∈ Possibility c,
 110    J y.value = J (Actualize c).value → p y
 111
 112/-- Determined properties are necessary among cost-equivalents. -/
 113theorem determined_necessary_for_minimal (p : ConfigProp) (c : Config)
 114    (hd : Determined p c) :
 115    ∀ y ∈ Possibility c, J y.value = J (Actualize c).value → p y :=
 116  hd
 117
 118/-! ## Path Action and Born Rule -/
 119
 120/-- **PATH ACTION**: The total J-cost accumulated along a path.
 121
 122    C[γ] = Σᵢ J(γᵢ) + J_transition(γᵢ, γᵢ₊₁)
 123
 124    This is the Recognition Science analogue of the classical action. -/
 125def PathAction (path : List Config) : ℝ :=
 126  match path with
 127  | [] => 0
 128  | [c] => J c.value
 129  | c₁ :: c₂ :: rest =>
 130      J c₁.value + J_transition c₁.value c₂.value c₁.pos c₂.pos +
 131      PathAction (c₂ :: rest)