CandidateLevelHistory.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The literal chronological history of a completed candidate level

The parent sequences append their actual records to one shared history. The concatenated group ordinal identifies both the stored record and exactly the prefix used to choose its budget, compact prediction set and detector.

def OAI.ReflexiveFixedPoints.CandidateContext.stageReturn line 30
Source documentation
The actual parent sequence at a natural stage of the level recursion.
```
def stageReturn (n : ℕ) :
    C.ParentReturn (C.parentAt n) (C.levelStates A hanchor hτ n) τ :=
…
```
def OAI.ReflexiveFixedPoints.CandidateContext.stageRecords line 34
def OAI.ReflexiveFixedPoints.CandidateContext.groupN line 38
Source documentation
The number of candidates actually selected for each parent.
```
def groupN (p : Fin C.frontier.size) : ℕ := (C.group A hanchor hτ p).N
```
theorem OAI.ReflexiveFixedPoints.CandidateContext.stageRecords_length line 40

theorem OAI.ReflexiveFixedPoints.CandidateContext.levelStates_succ_entries line 45

Source documentation

This is the append equation of the concrete selected sequence.

theorem levelStates_succ_entries (n : ℕ) :
    (C.levelStates A hanchor hτ (n + 1)).entries =
      (C.levelStates A hanchor hτ n).entries ++ C.stageRecords A hanchor hτ n :=
…

theorem OAI.ReflexiveFixedPoints.CandidateContext.levelStates_prefix line 50
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelStates_length line 57
Source documentation
The length counts every selected record, before discarding zero weights.
```
theorem levelStates_length (n : ℕ) :
    (C.levelStates A hanchor hτ n).entries.length =
      ∑ i : Fin n, (C.stageReturn A hanchor hτ i.val).N := by
…
```
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelStates_length_eq_prefix line 71
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelStates_length_eq_offset line 78
Source documentation
The state before a parent group has exactly the preceding groups' size.
```
theorem levelStates_length_eq_offset (p : Fin C.frontier.size) :
    (C.levelStates A hanchor hτ p.val).entries.length =
      OrderedGroupConcat.offset (C.groupN A hanchor hτ) p := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset
theorem OAI.ReflexiveFixedPoints.CandidateContext.finalState_length_eq_total line 87
Source documentation
The final history consists of exactly all candidate groups.
```
theorem finalState_length_eq_total :
    (C.finalState A hanchor hτ).entries.length =
      OrderedGroupConcat.total (C.groupN A hanchor hτ) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.CandidateContext.group_finalState_eq line 94
theorem OAI.ReflexiveFixedPoints.CandidateContext.group_finalState_prefix line 98

theorem OAI.ReflexiveFixedPoints.CandidateContext.group_state_length line 105

Source documentation

The state before a local candidate has its actual global ordinal as length.

theorem group_state_length (p : Fin C.frontier.size)
    (i : Fin (C.group A hanchor hτ p).N) :
    ((C.group A hanchor hτ p).state i.castSucc).entries.length =
      OrderedGroupConcat.offset (C.groupN A hanchor hτ) p + i.val := by
…

Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset

theorem OAI.ReflexiveFixedPoints.CandidateContext.group_state_eq_final_take line 115

Source documentation

Later groups do not alter the prefix used by this candidate.

theorem group_state_eq_final_take (p : Fin C.frontier.size)
    (i : Fin (C.group A hanchor hτ p).N) :
    ((C.group A hanchor hτ p).state i.castSucc).entries =
      (C.finalState A hanchor hτ).entries.take
        (OrderedGroupConcat.offset (C.groupN A hanchor hτ) p + i.val) := by
…

Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset

theorem OAI.ReflexiveFixedPoints.CandidateContext.finalState_get_groupRecord line 131

Source documentation

The actual global entry at a group coordinate is its originally chosen record.

theorem finalState_get_groupRecord (p : Fin C.frontier.size)
    (i : Fin (C.group A hanchor hτ p).N) :
    (C.finalState A hanchor hτ).entries[
      OrderedGroupConcat.offset (C.groupN A hanchor hτ) p + i.val]'(by
        rw [C.finalState_length_eq_total A hanchor hτ]
        exact (OrderedGroupConcat.group (C.groupN A hanchor hτ) p i).isLt) =
      (C.group A hanchor hτ p).record i := by
…

Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset, OAI.ReflexiveFixedPoints.OrderedGroupConcat.group

def OAI.ReflexiveFixedPoints.CandidateContext.levelRecord line 148
Source documentation
Decode the actual concatenated ordinal into its originally chosen record.
```
def levelRecord (i : Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ))) :
    CandidateRecord C :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total, OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelRecord_group line 153
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelRecord_parent line 164
theorem OAI.ReflexiveFixedPoints.CandidateContext.finalState_get_levelRecord line 178
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelRecord_legal line 195
Source documentation
Legality remains relative to the exact full candidate prefix.
```
theorem levelRecord_legal
    (i : Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ))) :
    C.Legal ((C.finalState A hanchor hτ).entries.take i.val)
      (C.levelRecord A hanchor hτ i) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.CandidateContext.prefix_nextOrdinal line 204
theorem OAI.ReflexiveFixedPoints.CandidateContext.prefix_nextBudget line 212

theorem OAI.ReflexiveFixedPoints.CandidateContext.levelRecord_spec line 220

Source documentation

Detector and full proper-ancestor estimates for the actual stored record.

theorem levelRecord_spec
    (i : Fin (OrderedGroupConcat.total (C.groupN A hanchor hτ))) :
    ‖(C.levelRecord A hanchor hτ i).functional‖ ≤ 1 ∧
    (∀ z ∈ C.detectorSet ((C.finalState A hanchor hτ).entries.take i.val),
      1 - candidateBudget (C.base + i.val) ≤
        (C.levelRecord A hanchor hτ i).functional
          (((C.levelRecord A hanchor hτ i).map C.anchor : X) - z)) ∧
    (∑ j : Fin (C.candidateAncestors (C.levelRecord A hanchor hτ i).parent).length,
      ‖(C.candidateAncestorMap (C.levelRecord A hanchor hτ i).parent j
          ((C.levelRecord A hanchor hτ i).map C.anchor) : X) -
        ((C.levelRecord A hanchor hτ i).map C.anchor : X)‖) ≤
      candidateBudget (C.base + i.val) := by
…

Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total, OAI.ReflexiveFixedPoints.candidateBudget