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

recognize

show as:
view Lean formalization →

The recognize definition implements the atomic recognition step in the cursor model by constructing a new ProofState that moves the current proposition into the verified set and advances the cursor to a chosen next proposition from the unverified set. Researchers working on the Recognition Science account of consciousness or free will would cite it as the primitive transition that advances the verification frontier while preserving the disjointness invariants. The definition proceeds by direct record construction followed by short simp-based re

claimLet $s$ be a ProofState with verified set $V$, current proposition $p$, and unverified set $U$, satisfying the invariants $pnotin V$ and $pnotin U$. Given a proposition $q$ such that $qin U$, $qneq p$, and $p$ holds, the recognition step returns the ProofState whose verified set is $Vcup{p}$, whose current proposition is $q$, and whose unverified set is $Usetminus{q}$, together with the updated invariants that the new current lies outside both the new verified set and the new unverified set.

background

The RRF Foundation module models consciousness as the active cursor that verifies propositions. ProofState encodes this cursor explicitly: the verified field holds the immutable past, the current field holds the proposition under active verification (the present), and the unverified field holds candidate propositions (the future). The structure maintains the invariant that these three components are pairwise disjoint. The module documentation states that consciousness is the verification step itself and that free will consists of constrained choice among valid moves. Upstream results such as the consistent predicate supply semantic compatibility checks that align with the state transition performed here.

proof idea

The definition builds a fresh ProofState record by setting verified to the union of the old verified set with the old current proposition, setting current to the supplied next proposition, and setting unverified to the old unverified set minus next. The current_not_in_past invariant is discharged by case analysis on membership in the union, invoking the original future_not_verified property of $s$. The current_not_in_future and future_not_verified invariants are established by direct set-difference simplification using simp and trivial.

why it matters in Recognition Science

This definition supplies the core transition operation for the consciousness cursor and is invoked by downstream results including cosmological_constant_resolution and unity_is_unique_existent. It realizes the free-will fragment of the model by permitting any valid next proposition while preserving the ledger invariants. Within the Recognition Science framework it corresponds to the active edge of recognition, linking the verification step to the J-cost interpretation of qualia and the strain-based account of pleasure and pain.

scope and limits

Lean usage

example (s : ProofState) (next : Prop) (h_next : next ∈ s.unverified) (h_ne : next ≠ s.current) (h_cur : s.current) : ProofState := recognize s next h_next h_ne h_cur

formal statement (Lean)

  53def recognize (s : ProofState) (next : Prop)
  54    (h_next : next ∈ s.unverified)
  55    (h_next_ne : next ≠ s.current)
  56    (_h_current_true : s.current) : ProofState := {

proof body

Definition body.

  57  verified := s.verified ∪ {s.current},
  58  current := next,
  59  unverified := s.unverified \ {next},
  60  current_not_in_past := by
  61    simp only [Set.mem_union, Set.mem_singleton_iff]
  62    intro h
  63    cases h with
  64    | inl h => exact s.future_not_verified next h_next h
  65    | inr h => exact absurd h h_next_ne
  66  current_not_in_future := by
  67    -- Goal: next ∉ s.unverified \ {next}
  68    -- This is true because we remove next from s.unverified
  69    simp only [Set.mem_diff, Set.mem_singleton_iff, not_and, not_not]
  70    intro _
  71    trivial
  72  future_not_verified := by
  73    intro p hp hv
  74    simp only [Set.mem_diff, Set.mem_singleton_iff] at hp
  75    simp only [Set.mem_union, Set.mem_singleton_iff] at hv
  76    cases hv with
  77    | inl h => exact s.future_not_verified p hp.1 h
  78    | inr h =>
  79      -- p = s.current, but hp says p ∈ s.unverified \ {next}
  80      -- So p ∈ s.unverified. But s.current ∉ s.unverified by current_not_in_future
  81      rw [h] at hp
  82      exact s.current_not_in_future hp.1
  83}
  84
  85/-! ## Valid Moves (Free Will) -/
  86
  87/-- A proposition is consistent with verified history. -/

used by (15)

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

depends on (12)

Lean names referenced from this declaration's body.