CandidateTreeTolerance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact tolerance for the actual recursively constructed tree

Every earlier retained candidate ordinal precedes the counter at the current finite stage. Thus the conservative scale used by actual adaptive selection is bounded by the precise retained-budget tolerance, which is the scale exported by the tree construction.

theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.runTolerance_le_tolerance line 24
Source documentation
The actual requested return accuracy implies the exact scale.
```
theorem runTolerance_le_tolerance (k : ℕ) :
    (context D A U k).runTolerance ≤
      (tower D A U).toOrderedTree.tolerance
        (OrderedTree.retainedBudget (candidateLabel D A U)) k := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower_child_average line 35
Source documentation
Every actual parent has the required child-average estimate in the original normalized norm, with the exact retained-budget tolerance.
```
theorem tower_child_average (k : ℕ)
    (p : (tower D A U).toOrderedTree.Node k) :
    ‖((tower D A U).toEvaluation.childAverage k
      (fun v => (tower D A U).toEvaluation.map (k + 1) v A.x) p : X) - (A.x : X)‖ ≤
      (tower D A U).toOrderedTree.tolerance
        (OrderedTree.retainedBudget (candidateLabel D A U)) k :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel