pith. machine review for the scientific record. sign in
def definition def or abbrev

validMoves

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  93def validMoves (s : ProofState) : Set Prop :=

proof body

Definition body.

  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. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.