FrontierTower.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

From actual finite extensions to one infinite evaluated tree

A tower records the concrete successor extension at every finite stage. Its coherence equalities identify each new frontier with that extension. The infinite tree, its positive weights, and its nonlinear evaluation are extracted from these records. Finite and infinite evaluation agree by induction on the number of extensions.

theorem OAI.ReflexiveFixedPoints.TreeFrontier.map_transport line 30
Source documentation
Transport a node map through equality of the concrete frontiers.
```
theorem map_transport {F G : TreeFrontier K} (h : F = G) (p : Fin F.size) :
    F.map p = G.map (finCongr (congrArg TreeFrontier.size h) p) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeFrontier
theorem OAI.ReflexiveFixedPoints.TreeFrontier.evaluate_transport line 36
Source documentation
Transport a cutoff assignment through equality of concrete frontiers.
```
theorem evaluate_transport {F G : TreeFrontier K} (h : F = G)
    (H : Fin F.size → K) :
    F.evaluate H =
      G.evaluate (fun p => H ((finCongr (congrArg TreeFrontier.size h)).symm p)) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeFrontier
theorem OAI.ReflexiveFixedPoints.TreeFrontier.evaluate_eq_root_of_eq line 43
theorem OAI.ReflexiveFixedPoints.TreeFrontier.map_eq_id_of_eq_root line 49
structure OAI.ReflexiveFixedPoints.FrontierTower line 57
Source documentation
A coherent sequence of actual finite extensions, beginning with the root.
```
structure FrontierTower (K : Set X) where
…
```
theorem OAI.ReflexiveFixedPoints.FrontierTower.next_size line 68
def OAI.ReflexiveFixedPoints.FrontierTower.nextNode line 72
Source documentation
The canonical identification of next-level nodes with the actual extension.
```
def nextNode (k : ℕ) : Fin (S.frontier (k + 1)).size ≃ Fin (S.step k).size :=
…
```
theorem OAI.ReflexiveFixedPoints.FrontierTower.nextNode_val line 75
theorem OAI.ReflexiveFixedPoints.FrontierTower.nextNode_symm_val line 78
theorem OAI.ReflexiveFixedPoints.FrontierTower.nextNode_monotone line 81
def OAI.ReflexiveFixedPoints.FrontierTower.toOrderedTree line 86
Source documentation
The single infinite ordered tree extracted from all concrete levels.
```
def toOrderedTree : OrderedTree where
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree
theorem OAI.ReflexiveFixedPoints.FrontierTower.toOrderedTree_size line 94
theorem OAI.ReflexiveFixedPoints.FrontierTower.toOrderedTree_parent line 97
def OAI.ReflexiveFixedPoints.FrontierTower.toWeightedTree line 101
Source documentation
Extract the actual positive weights chosen by every finite extension.
```
def toWeightedTree : WeightedTree S.toOrderedTree where
…
```
Mentions: OAI.ReflexiveFixedPoints.WeightedTree
theorem OAI.ReflexiveFixedPoints.FrontierTower.toWeightedTree_weight line 115
def OAI.ReflexiveFixedPoints.FrontierTower.toEvaluation line 119
Source documentation
The final nonlinear evaluator uses exactly the maps stored in the frontiers.
```
def toEvaluation : TreeEvaluation S.toWeightedTree K where
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeEvaluation
theorem OAI.ReflexiveFixedPoints.FrontierTower.toEvaluation_map line 124
theorem OAI.ReflexiveFixedPoints.FrontierTower.toEvaluation_map_succ line 127
theorem OAI.ReflexiveFixedPoints.FrontierTower.toEvaluation_map_zero line 131

theorem OAI.ReflexiveFixedPoints.FrontierTower.childAverage_agreement line 136

Source documentation

Reindexing the new children preserves their actual convex average.

theorem childAverage_agreement (k : ℕ) (H : S.toOrderedTree.Node (k + 1) → K)
    (p : S.toOrderedTree.Node k) :
    S.toEvaluation.childAverage k H p =
      (S.step k).childAverage (fun c => H ((S.nextNode k).symm c)) p := by
…

theorem OAI.ReflexiveFixedPoints.FrontierTower.collapse_agreement line 150
theorem OAI.ReflexiveFixedPoints.FrontierTower.frontier_zero_evaluate line 158

theorem OAI.ReflexiveFixedPoints.FrontierTower.frontier_succ_evaluate line 163

Source documentation

Successor frontier evaluation is its recorded predecessor composition.

theorem frontier_succ_evaluate (k : ℕ) (H : S.toOrderedTree.Node (k + 1) → K) :
    (S.frontier (k + 1)).evaluate H =
      (S.frontier k).evaluate
        ((S.step k).collapse (fun c => H ((S.nextNode k).symm c))) :=
…

theorem OAI.ReflexiveFixedPoints.FrontierTower.evaluate_agreement line 170
Source documentation
The finite prediction evaluator equals the final infinite-tree evaluator.
```
theorem evaluate_agreement (k : ℕ) (H : S.toOrderedTree.Node k → K) :
    (S.frontier k).evaluate H = S.toEvaluation.evaluate k H := by
…
```

theorem OAI.ReflexiveFixedPoints.FrontierTower.evaluate_map_agreement line 187

Source documentation

Agreement also holds after applying each already chosen cutoff map once.

theorem evaluate_map_agreement (k : ℕ) (H : S.toOrderedTree.Node k → K) :
    (S.frontier k).evaluate (fun p => (S.frontier k).map p (H p)) =
      S.toEvaluation.evaluate k (fun p => S.toEvaluation.map k p (H p)) :=
…