CandidateTolerance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Conservative candidate scales imply the exact retained-budget tolerance

The construction may request a smaller return tolerance, using its complete candidate counter. Every retained earlier ordinal is at most that counter, so its geometric budget bounds this requested scale from below. The exposed tolerance remains the exact dyadic multiple of the retained-budget minimum.

theorem OAI.ReflexiveFixedPoints.candidateBudget_antitone line 17
theorem OAI.ReflexiveFixedPoints.OrderedTree.candidateBudget_le_cumulativeMinimum line 29
Source documentation
A counter beyond all preceding labels supplies a lower bound for their actual finite minimum. The zero-depth case is included.
```
theorem candidateBudget_le_cumulativeMinimum (k counter : ℕ)
    (hcounter : ∀ i < k, ∀ v : T.Node (i + 1), label ⟨i, v⟩ ≤ counter) :
    candidateBudget counter ≤ T.cumulativeMinimum (retainedBudget label) k := by
…
```
Mentions: OAI.ReflexiveFixedPoints.candidateBudget, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget
theorem OAI.ReflexiveFixedPoints.OrderedTree.candidateScale_le_tolerance line 40
Source documentation
The actual requested selection scale is no larger than the exact retained-budget tolerance specified by the retained budgets.
```
theorem candidateScale_le_tolerance (k counter : ℕ)
    (hcounter : ∀ i < k, ∀ v : T.Node (i + 1), label ⟨i, v⟩ ≤ counter) :
    (1 / 2 : ℝ) ^ (k + 1) * candidateBudget counter ≤
      T.tolerance (retainedBudget label) k := by
…
```
Mentions: OAI.ReflexiveFixedPoints.candidateBudget, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget
theorem OAI.ReflexiveFixedPoints.OrderedTree.candidateScale_le_tolerance_of_lt line 49
Source documentation
Strictly earlier candidate ordinals are a sufficient chronological bound.
```
theorem candidateScale_le_tolerance_of_lt (k counter : ℕ)
    (hcounter : ∀ i < k, ∀ v : T.Node (i + 1), label ⟨i, v⟩ < counter) :
    (1 / 2 : ℝ) ^ (k + 1) * candidateBudget counter ≤
      T.tolerance (retainedBudget label) k :=
…
```
Mentions: OAI.ReflexiveFixedPoints.candidateBudget, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget