TreeBudget.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Budgets attached to retained candidate ordinals

The label of a retained node is its zero-based ordinal in the global candidate sequence. Thus the one-based label ℓ = label + 1 gives the budget 2 ^ (-ℓ - 8) = (1 / 2) ^ (label + 9). Injectivity, rather than a new enumeration of retained nodes, compares their total with the candidate series. The actual tree construction supplies this label and its injectivity proof.

def OAI.ReflexiveFixedPoints.candidateBudget line 24
Source documentation
The dyadic budget of the candidate with zero-based ordinal n.
```
def candidateBudget (n : ℕ) : ℝ := (1 / 2 : ℝ) ^ (n + 9)
```
theorem OAI.ReflexiveFixedPoints.candidateBudget_pos line 26
theorem OAI.ReflexiveFixedPoints.candidateBudget_nonneg line 29
theorem OAI.ReflexiveFixedPoints.candidateBudget_le_one line 32
theorem OAI.ReflexiveFixedPoints.hasSum_candidateBudget line 36
Source documentation
The complete candidate series has sum exactly 1 / 256.
```
theorem hasSum_candidateBudget : HasSum candidateBudget (1 / 256 : ℝ) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.candidateBudget
theorem OAI.ReflexiveFixedPoints.summable_candidateBudget line 43
theorem OAI.ReflexiveFixedPoints.tsum_candidateBudget line 46
abbrev OAI.ReflexiveFixedPoints.OrderedTree.NonrootNode line 52
Source documentation
Every nonroot node, retaining its actual positive level.
```
abbrev NonrootNode (T : OrderedTree) := Σ k : ℕ, T.Node (k + 1)
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree
def OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget line 57
Source documentation
The retained budget uses the original global candidate label.
```
def retainedBudget (label : T.NonrootNode → ℕ) (v : T.NonrootNode) : ℝ :=
…
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget_pos line 60
theorem OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget_nonneg line 64
theorem OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget_le_one line 68
theorem OAI.ReflexiveFixedPoints.OrderedTree.summable_retainedBudget line 74
Source documentation
Retaining a subset of globally distinct candidate labels preserves summability. No bound on the number of nodes at later levels is needed.
```
theorem summable_retainedBudget (label : T.NonrootNode → ℕ)
    (hlabel : Function.Injective label) : Summable (retainedBudget label) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget
theorem OAI.ReflexiveFixedPoints.OrderedTree.tsum_retainedBudget_le line 79
Source documentation
The total retained budget is at most the complete candidate budget.
```
theorem tsum_retainedBudget_le (label : T.NonrootNode → ℕ)
    (hlabel : Function.Injective label) :
    (∑' v, retainedBudget label v) ≤ (1 / 256 : ℝ) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget
theorem OAI.ReflexiveFixedPoints.OrderedTree.tsum_retainedBudget_le_one_div_128 line 87
theorem OAI.ReflexiveFixedPoints.OrderedTree.sum_retainedBudget_le line 93
Source documentation
Every finite retained selection satisfies the same global budget bound.
```
theorem sum_retainedBudget_le (label : T.NonrootNode → ℕ)
    (hlabel : Function.Injective label) (s : Finset T.NonrootNode) :
    (∑ v ∈ s, retainedBudget label v) ≤ (1 / 256 : ℝ) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget
theorem OAI.ReflexiveFixedPoints.OrderedTree.sum_retainedBudget_comp_le line 104
Source documentation
A finite truncation, or any finite injectively indexed collection of actual nonroot nodes, satisfies the complete retained budget bound.
```
theorem sum_retainedBudget_comp_le {ι : Type*} [Fintype ι]
    (label : T.NonrootNode → ℕ) (hlabel : Function.Injective label)
    (node : ι → T.NonrootNode) (hnode : Function.Injective node) :
    (∑ i, retainedBudget label (node i)) ≤ (1 / 256 : ℝ) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget