validMoves

formal source

  90  ∀ q ∈ verified, ¬(p = ¬q)
  91
  92/-- Valid next moves: consistent with history. -/
  93def validMoves (s : ProofState) : Set Prop :=
  94  { p ∈ s.unverified | isConsistent s.verified p }
  95
  96/-- **HYPOTHESIS**: Free will as choice among valid moves.
  97
  98    STATUS: SCAFFOLD — While existence of valid moves is formally
  99    defined as consistency with verified history, the mechanism of
 100    conscious choice ("free will") is a core postulate of the model.
 101
 102    TODO: Formally define the choice operator and its relationship to J-cost. -/
 103def H_FreeWillExists (s : ProofState) : Prop :=
 104  (validMoves s).Nonempty →
 105    ∃ p, p ∈ validMoves s -- SCAFFOLD: Needs formal choice mechanism.
 106
 107/-- Free will: if valid moves exist, we can choose among them. -/
 108theorem free_will_exists (s : ProofState)
 109    (h : (validMoves s).Nonempty) :
 110    ∃ p, p ∈ validMoves s := by
 111  obtain ⟨p, hp⟩ := h
 112  exact ⟨p, hp⟩
 113
 114/-- Determinism: we can only move to states reachable via recognize. -/
 115theorem determinism_constraint (s : ProofState) (next : Prop)
 116    (h_next : next ∈ s.unverified) (h_ne : next ≠ s.current) (h_true : s.current) :
 117    (recognize s next h_next h_ne h_true).current = next := rfl
 118
 119/-! ## Qualia as Strain -/
 120
 121/-- A qualia state: strain and valence with identity constraint.
 122
 123The key insight: valence IS negative strain, not caused by it.