CandidateRecords.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Candidate records and their immutable preceding history

The detector set of a new record is computed from the entire preceding list. This list includes records which will later receive coefficient zero. No coefficient, retained child list, or future frontier occurs in that set.

abbrev OAI.ReflexiveFixedPoints.GeneratedSelfMap line 27
Source documentation
A genuine generated selfmap, carrying the proof of its origin.
```
abbrev GeneratedSelfMap (D : NormalizedMinimalData (X := X)) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData
structure OAI.ReflexiveFixedPoints.CandidateContext line 31
Source documentation
Data already fixed when construction of a new finite level starts.
```
structure CandidateContext (D : NormalizedMinimalData (X := X)) where
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData
structure OAI.ReflexiveFixedPoints.CandidateRecord line 43
Source documentation
The auxiliary functional is chosen after this actual map has been selected. The budget and detector set are derived from the record's prefix.
```
structure CandidateRecord {D : NormalizedMinimalData (X := X)}
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData
def OAI.ReflexiveFixedPoints.CandidateContext.nextOrdinal line 55
Source documentation
The globally fresh zero-based label before a candidate is chosen.
```
def nextOrdinal (history : List (CandidateRecord C)) : ℕ := C.base + history.length
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
def OAI.ReflexiveFixedPoints.CandidateContext.nextBudget line 58
Source documentation
The next budget is fixed by the full history, including discarded maps.
```
def nextBudget (history : List (CandidateRecord C)) : ℝ :=
…
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.nextBudget_pos line 61
def OAI.ReflexiveFixedPoints.CandidateContext.historyParent line 65
Source documentation
Earlier parent labels, read without changing their order.
```
def historyParent (history : List (CandidateRecord C))
    (i : Fin history.length) : Fin C.frontier.size := (history.get i).parent
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
def OAI.ReflexiveFixedPoints.CandidateContext.historyPoint line 69
Source documentation
Earlier candidate outputs at the fixed anchor.
```
def historyPoint (history : List (CandidateRecord C))
    (i : Fin history.length) : D.K := (history.get i).map C.anchor
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
def OAI.ReflexiveFixedPoints.CandidateContext.detectorSet line 73
Source documentation
The actual compact prediction detector, computed before the next map.
```
def detectorSet (history : List (CandidateRecord C)) : Set X :=
…
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.detectorSet_nonempty line 78
theorem OAI.ReflexiveFixedPoints.CandidateContext.detectorSet_subset line 84
theorem OAI.ReflexiveFixedPoints.CandidateContext.isCompact_detectorSet line 90
def OAI.ReflexiveFixedPoints.CandidateContext.ancestorMap line 99
Source documentation
The actual maps on the fixed path to a parent.
```
def ancestorMap (p : Fin C.frontier.size)
    (i : Fin (C.ancestors p).length) : D.K → D.K := ((C.ancestors p).get i).val
```
theorem OAI.ReflexiveFixedPoints.CandidateContext.ancestorMap_generated line 102
def OAI.ReflexiveFixedPoints.CandidateContext.candidateAncestors line 108
Source documentation
Proper ancestors of a new child include its current parent map.
```
def candidateAncestors (p : Fin C.frontier.size) : List (GeneratedSelfMap D) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.GeneratedSelfMap
def OAI.ReflexiveFixedPoints.CandidateContext.candidateAncestorMap line 111
theorem OAI.ReflexiveFixedPoints.CandidateContext.candidateAncestorMap_generated line 115
def OAI.ReflexiveFixedPoints.CandidateContext.Legal line 121
Source documentation
Legality is relative to the exact immutable preceding prefix.
```
def Legal (history : List (CandidateRecord C)) (r : CandidateRecord C) : Prop :=
…
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.nextOrdinal_append line 129
theorem OAI.ReflexiveFixedPoints.CandidateContext.nextOrdinal_lt_append line 134