  68  minimizes_cost : ∀ y ∈ Possibility current, J successor.value ≤ J y.value
  69
  70/-- An actualization witness for a configuration. -/
  71def has_actualization (c : Config) : Prop :=
  72  ∃ ap : ActualizationPrinciple, ap.current = c
  73
  74/-- Every configuration has an actualization (toward identity). -/
  75theorem every_config_actualizes (c : Config) : has_actualization c := by
  76  use {
  77    current := c
  78    successor := identity_config (c.time + 8)
  79    in_possibility := identity_always_possible c
  80    minimizes_cost := by
  81      intro y hy
  82      simp [identity_config, J_at_one]
  83      exact J_nonneg y.pos
  84  }
  85
  86/-! ## Degeneracy and Contingency -/
  87
  88/-- **DEGENERACY**: When multiple configurations have the same minimal cost.
  89
  90    This is the origin of contingency in RS—when the universe "could have gone either way"
  91    because multiple paths have identical J-cost. -/
  92def Degenerate (c : Config) : Prop :=
  93  ∃ y ∈ Possibility c, ∃ z ∈ Possibility c, y ≠ z ∧ J y.value = J z.value ∧
  94    ∀ w ∈ Possibility c, J y.value ≤ J w.value
  95
  96/-- **CONTINGENT**: A property that could have been otherwise.
  97
  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 :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.