SequentialHistory.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Immutable histories whose new entry is checked against the complete past

Each stored entry is legal for its exact preceding list. Later appends preserve that past, so data chosen before current weights cannot be retrospectively changed by removing candidates.

inductive OAI.ReflexiveFixedPoints.SequentialHistory line 18

Source documentation

Validity records chronology, not merely membership in an unordered set.

inductive SequentialHistory {R : Type u} (legal : List R → R → Prop) : List R → Prop
  | nil : SequentialHistory legal []
  | snoc {past : List R} {entry : R} :
      SequentialHistory legal past → legal past entry →
        SequentialHistory legal (past ++ [entry])

namespace SequentialHistory

variable {R : Type u} {legal : List R → R → Prop}

/-- Every entry was admitted using its exact earlier prefix. -/

theorem OAI.ReflexiveFixedPoints.SequentialHistory.legal_get line 29
Source documentation
Every entry was admitted using its exact earlier prefix.
```
theorem legal_get {entries : List R} (h : SequentialHistory legal entries)
    (i : ℕ) (hi : i < entries.length) :
    legal (entries.take i) entries[i] := by
…
```
Mentions: OAI.ReflexiveFixedPoints.SequentialHistory
theorem OAI.ReflexiveFixedPoints.SequentialHistory.take line 48
Source documentation
Every initial segment remains a valid history.
```
theorem take {entries : List R} (h : SequentialHistory legal entries) (n : ℕ) :
    SequentialHistory legal (entries.take n) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.SequentialHistory
structure OAI.ReflexiveFixedPoints.HistoryState line 62
Source documentation
A state type in which every possible state already has a legal complete history.
```
structure HistoryState (R : Type u) (legal : List R → R → Prop) where
…
```
def OAI.ReflexiveFixedPoints.HistoryState.empty line 71
Source documentation
Start with the empty chronological history.
```
def empty : HistoryState R legal := ⟨[], SequentialHistory.nil⟩
```
Mentions: OAI.ReflexiveFixedPoints.HistoryState
def OAI.ReflexiveFixedPoints.HistoryState.append line 74
Source documentation
Append one newly chosen record without changing any previous record.
```
def append (s : HistoryState R legal) (entry : R) (h : legal s.entries entry) :
    HistoryState R legal :=
…
```
Mentions: OAI.ReflexiveFixedPoints.HistoryState
theorem OAI.ReflexiveFixedPoints.HistoryState.append_entries line 78
theorem OAI.ReflexiveFixedPoints.HistoryState.append_length line 82

theorem OAI.ReflexiveFixedPoints.HistoryState.append_get_old line 88

Source documentation

Earlier records are preserved literally.

theorem append_get_old (s : HistoryState R legal) (entry : R)
    (h : legal s.entries entry) (i : ℕ) (hi : i < s.entries.length) :
    (s.append entry h).entries[i]'(by simpa using Nat.lt_succ_of_lt hi) = s.entries[i] := by
…

Mentions: OAI.ReflexiveFixedPoints.HistoryState

theorem OAI.ReflexiveFixedPoints.HistoryState.append_take_old line 94

Source documentation

The prefix used to choose an earlier record is preserved literally.

theorem append_take_old (s : HistoryState R legal) (entry : R)
    (h : legal s.entries entry) (n : ℕ) (hn : n ≤ s.entries.length) :
    (s.append entry h).entries.take n = s.entries.take n :=
…

Mentions: OAI.ReflexiveFixedPoints.HistoryState

theorem OAI.ReflexiveFixedPoints.HistoryState.legal_get line 100
Source documentation
Recover the exact preceding-history law for any actual stored entry.
```
theorem legal_get (s : HistoryState R legal) (i : ℕ) (hi : i < s.entries.length) :
    legal (s.entries.take i) s.entries[i] := s.valid.legal_get i hi
…
```
Mentions: OAI.ReflexiveFixedPoints.HistoryState