CandidateAncestors.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The stored ancestor lists are the actual paths of the constructed tree

The stage recursion appends the current parent's map to its stored strict ancestor list. This is exactly the recursion defining pathDisplacement. The finite sums used when selecting candidates therefore bound the final tree's actual proper-ancestor displacement.

theorem OAI.ReflexiveFixedPoints.CandidateContext.ancestorMap_sum_eq_list line 31

Source documentation

Reading a stored ancestor list by finite indices gives its literal list sum.

theorem ancestorMap_sum_eq_list (p : Fin C.frontier.size) (z : D.K) :
    (∑ i : Fin (C.ancestors p).length, ‖(C.ancestorMap p i z : X) - z‖) =
      ((C.ancestors p).map (fun g => ‖(g.val z : X) - z‖)).sum := by
…

theorem OAI.ReflexiveFixedPoints.CandidateContext.candidateAncestorMap_sum_eq_list line 37

theorem OAI.ReflexiveFixedPoints.CandidateContext.candidateAncestorMap_sum_eq line 45

Source documentation

A new child's proper ancestors include its current parent's map.

theorem candidateAncestorMap_sum_eq (p : Fin C.frontier.size) (z : D.K) :
    (∑ i : Fin (C.candidateAncestors p).length,
      ‖(C.candidateAncestorMap p i z : X) - z‖) =
      (∑ i : Fin (C.ancestors p).length, ‖(C.ancestorMap p i z : X) - z‖) +
        ‖(C.frontier.map p z : X) - z‖ := by
…

theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_ancestors_succ line 63
Source documentation
The actual successor list appends the final tree's current parent map.
```
theorem context_ancestors_succ (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    (context D A U (k + 1)).ancestors v =
      (context D A U k).candidateAncestors ((tower D A U).toOrderedTree.parent k v) := rfl
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.ancestorList_displacement_eq line 69
Source documentation
List recursion and actual path recursion compute the same displacement.
```
theorem ancestorList_displacement_eq (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node k) (z : D.K) :
    (((context D A U k).ancestors v).map (fun g => ‖(g.val z : X) - z‖)).sum =
      (tower D A U).toEvaluation.pathDisplacement k v z := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.ancestorMap_sum_eq_pathDisplacement line 91
Source documentation
The exact finite sum over stored strict ancestors equals the final path sum.
```
theorem ancestorMap_sum_eq_pathDisplacement (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node k) (z : D.K) :
    (∑ i : Fin ((context D A U k).ancestors v).length,
      ‖((context D A U k).ancestorMap v i z : X) - z‖) =
      (tower D A U).toEvaluation.pathDisplacement k v z := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context

theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateAncestorMap_sum_eq_pathDisplacement line 101

Source documentation

The candidate-selection ancestor sum is exactly the path sum of its new child.

theorem candidateAncestorMap_sum_eq_pathDisplacement (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) (z : D.K) :
    (∑ i : Fin ((context D A U k).candidateAncestors
        ((tower D A U).toOrderedTree.parent k v)).length,
      ‖((context D A U k).candidateAncestorMap
        ((tower D A U).toOrderedTree.parent k v) i z : X) - z‖) =
      (tower D A U).toEvaluation.pathDisplacement (k + 1) v z := by
…

Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context