CandidateLevel.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

A concrete sequential construction of one finite level

Parents are visited in their finite order. Each adaptive return starts from the full final history of the preceding parent. The retained positive children are then concatenated into an actual frontier extension.

def OAI.ReflexiveFixedPoints.CandidateContext.parentAt line 27
Source documentation
A total parent index for the natural-number recursion. Only the first frontier.size stages are used to construct the finite level.
```
def parentAt (i : ℕ) : Fin C.frontier.size :=
…
```
theorem OAI.ReflexiveFixedPoints.CandidateContext.parentAt_fin line 30
def OAI.ReflexiveFixedPoints.CandidateContext.levelStates line 38
Source documentation
Successive parents share the complete chronological candidate history.
```
def levelStates : ℕ → C.State
  | 0 => HistoryState.empty
  | i + 1 =>
    let r := C.selectParent A hanchor (C.parentAt i)
…
```
Mentions: OAI.ReflexiveFixedPoints.HistoryState.empty
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelStates_zero line 45
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelStates_succ line 48
def OAI.ReflexiveFixedPoints.CandidateContext.group line 55
Source documentation
The actual return chosen while processing this parent.
```
def group (p : Fin C.frontier.size) :
    C.ParentReturn (C.parentAt p.val) (C.levelStates A hanchor hτ p.val) τ :=
…
```

theorem OAI.ReflexiveFixedPoints.CandidateContext.group_finalState line 60

Source documentation

The entire final state of a parent's return starts the next stage.

theorem group_finalState (p : Fin C.frontier.size) :
    (C.group A hanchor hτ p).state (Fin.last (C.group A hanchor hτ p).N) =
      C.levelStates A hanchor hτ (p.val + 1) := rfl

theorem OAI.ReflexiveFixedPoints.CandidateContext.group_map_generated line 65

Source documentation

Each retained child is the actual tail map selected by its parent's sequence.

theorem group_map_generated (p : Fin C.frontier.size)
    (j : Fin (C.group A hanchor hτ p).q) :
    Generated D.closed D.convex D.T D.nonexpansive
      ((C.group A hanchor hτ p).selected ((C.group A hanchor hτ p).retain j)) :=
…

Mentions: OAI.ReflexiveFixedPoints.Generated

theorem OAI.ReflexiveFixedPoints.CandidateContext.group_map_nonexpansive line 72
def OAI.ReflexiveFixedPoints.CandidateContext.levelExtension line 80
Source documentation
Assemble the retained positive children, in their original parent order.
```
def levelExtension : FrontierExtension C.frontier :=
…
```
Mentions: OAI.ReflexiveFixedPoints.FrontierExtension
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelExtension_size line 90
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelExtension_parent_group line 94
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelExtension_weight_group line 100
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelExtension_map_group line 115
theorem OAI.ReflexiveFixedPoints.CandidateContext.levelExtension_generated line 131
Source documentation
Every map in the assembled extension has its actual generation proof.
```
theorem levelExtension_generated (i : Fin (C.levelExtension A hanchor hτ).size) :
    Generated D.closed D.convex D.T D.nonexpansive
      ((C.levelExtension A hanchor hτ).map i) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.Generated

theorem OAI.ReflexiveFixedPoints.CandidateContext.levelExtension_childAverage_near line 139

Source documentation

The actual child averages return to the anchor with the chosen tolerance.

theorem levelExtension_childAverage_near (p : Fin C.frontier.size) :
    ‖((C.levelExtension A hanchor hτ).childAverage
      (fun i => (C.levelExtension A hanchor hτ).map i C.anchor) p : X) -
      (C.anchor : X)‖ < τ := by
…

def OAI.ReflexiveFixedPoints.CandidateContext.finalState line 149
Source documentation
The history after precisely one pass through all current parents.
```
def finalState : C.State := C.levelStates A hanchor hτ C.frontier.size
…
```