ParentReturnHistory.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Exact chronological records of a finite parent return

The returned adaptive transitions append actual records. Their full list, including records of coefficient zero, is recovered without changing the prefix against which any detector was chosen.

theorem OAI.ReflexiveFixedPoints.append_run_prefix line 21

Source documentation

A finite append sequence has its literal initial list followed by its records.

theorem append_run_prefix {R : Type*} {N : ℕ}
    (state : Fin (N + 1) → List R) (record : Fin N → R)
    (hstep : ∀ i : Fin N, state i.succ = state i.castSucc ++ [record i])
    (n : ℕ) (hn : n ≤ N) :
    state ⟨n, Nat.lt_succ_of_le hn⟩ =
      state ⟨0, Nat.succ_pos N⟩ ++
        List.ofFn (fun i : Fin n => record ⟨i, Nat.lt_of_lt_of_le i.isLt hn⟩) := by
…

def OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.record line 50
Source documentation
The actual record appended by this adaptive step.
```
def record (i : Fin R.N) : CandidateRecord C :=
…
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.record_parent line 53
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.record_map line 56
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.record_legal line 59
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.state_succ_entries line 64
Source documentation
No previous record is rewritten by a transition.
```
theorem state_succ_entries (i : Fin R.N) :
    (R.state i.succ).entries =
      (R.state i.castSucc).entries ++ [R.record i] := by
…
```

theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.state_entries line 72

Source documentation

The selected prefix has exactly the state recorded at that time.

theorem state_entries (n : ℕ) (hn : n ≤ R.N) :
    (R.state ⟨n, Nat.lt_succ_of_le hn⟩).entries = initial.entries ++
      List.ofFn (fun i : Fin n => R.record ⟨i, Nat.lt_of_lt_of_le i.isLt hn⟩) := by
…

theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.state_length line 80
Source documentation
Each candidate receives a fresh chronological position.
```
theorem state_length (n : ℕ) (hn : n ≤ R.N) :
    (R.state ⟨n, Nat.lt_succ_of_le hn⟩).entries.length =
      initial.entries.length + n := by
…
```
def OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.records line 87
Source documentation
The full candidate group retains every record, including discarded ones.
```
def records : List (CandidateRecord C) := List.ofFn R.record
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.records_length line 89
def OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.finalState line 92
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.finalState_entries line 94
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.finalState_length line 98

theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.finalState_get_record line 103

Source documentation

The exact stored record at its global position.

theorem finalState_get_record (i : Fin R.N) :
    R.finalState.entries[initial.entries.length + i.val]'(by
      rw [R.finalState_length]
      exact Nat.add_lt_add_left i.isLt _) = R.record i := by
…

theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.records_parent line 112
Source documentation
Every record of this group belongs to the one parent being processed.
```
theorem records_parent (r : CandidateRecord C) (hr : r ∈ R.records) : r.parent = p := by
…
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn.state_entries_eq_final_take line 119
Source documentation
An earlier state is exactly the corresponding prefix of the completed history.
```
theorem state_entries_eq_final_take (n : ℕ) (hn : n ≤ R.N) :
    (R.state ⟨n, Nat.lt_succ_of_le hn⟩).entries =
      R.finalState.entries.take (initial.entries.length + n) := by
…
```