SwitchingTreeData.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete tree-construction output consumed by switching

This record states the conclusions of the adaptive ordered-tree producer. Its candidate labels are the original global selection ordinals. Predictions are the actual evaluations of the ideal cutoff; the producer derives their weak limits and detectors from its full earlier-candidate families, with all discarded candidates retained. No field below is an additional hypothesis of the public original-norm fixed-point theorem.

structure OAI.ReflexiveFixedPoints.SwitchingTreeData line 30
def OAI.ReflexiveFixedPoints.SwitchingTreeData.budget line 69
Source documentation
Extend the nonroot budget by zero at the root, which has no detector.
```
def budget : (k : ℕ) → A.tree.Node k → ℝ
  | 0, _ => 0
  | k + 1, v => OrderedTree.retainedBudget A.label ⟨k, v⟩

/-- Extend the actual nonroot functionals by the zero functional at the root. -/
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget

def OAI.ReflexiveFixedPoints.SwitchingTreeData.functionalAt line 74

Source documentation

Extend the actual nonroot functionals by the zero functional at the root.

def functionalAt : (k : ℕ) → A.tree.Node k → X →L[ℝ] ℝ
  | 0, _ => 0
  | k + 1, v => A.functional k v

/-- The actual anchor images labelling every node of the tree. -/

def OAI.ReflexiveFixedPoints.SwitchingTreeData.nodeLabel line 79
Source documentation
The actual anchor images labelling every node of the tree.
```
def nodeLabel (k : ℕ) (v : A.tree.Node k) : D.K :=
…
```
def OAI.ReflexiveFixedPoints.SwitchingTreeData.terminal line 83
Source documentation
The single actual terminal sequence fixed for this constructed tree.
```
def terminal (j : ℕ) : D.K :=
…
```
theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.functionalAt_norm line 87
Source documentation
All extended functionals still have norm at most one.
```
theorem functionalAt_norm (k : ℕ) (v : A.tree.Node k) :
    ‖A.functionalAt k v‖ ≤ 1 := by
…
```
theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.budget_pos line 93
theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.summable_budget line 97