SwitchingStates.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Actual root states during right-to-left switching

At cutoff t, the leaves with index strictly below t retain their labels; all other leaves have the common terminal value. Decreasing t by one is one actual switch. Every increment below is a difference of these evaluated root states, so finite telescoping never assumes that a node map is linear.

def OAI.ReflexiveFixedPoints.TreeEvaluation.switchLeaves line 30
Source documentation
The actual leaf assignment after every leaf at or to the right of the cutoff has switched.
```
def switchLeaves (_E : TreeEvaluation W K) (N : ℕ) (y : T.Node N → K)
    (b : K) (t : ℕ) : T.Node N → K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeEvaluation
def OAI.ReflexiveFixedPoints.TreeEvaluation.switchRoot line 35
Source documentation
One fully evaluated actual root state of the switching experiment.
```
noncomputable def switchRoot (N : ℕ) (y : T.Node N → K) (b : K) (t : ℕ) : K :=
…
```
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchLeaves_zero line 38
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchLeaves_full line 43

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchLeaves_succ_eq_of_ne line 49

Source documentation

Two consecutive cutoff states differ only at the leaf being switched.

theorem switchLeaves_succ_eq_of_ne (N : ℕ) (y : T.Node N → K) (b : K)
    (s w : T.Node N) (hws : w ≠ s) :
    E.switchLeaves N y b (s.val + 1) w = E.switchLeaves N y b s.val w := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchRoot_single_norm_le line 58

Source documentation

The root increment of one leaf has its actual path weight as its norm bound.

theorem switchRoot_single_norm_le (N : ℕ) (y : T.Node N → K) (b : K)
    (s : T.Node N) :
    ‖(E.switchRoot N y b (s.val + 1) : X) - E.switchRoot N y b s.val‖ ≤
      W.pathWeight N s * ‖(y s : X) - b‖ := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchRoot_single_norm_le_weight line 69

Source documentation

Diameter one bounds the actual single-leaf root increment by its weight.

theorem switchRoot_single_norm_le_weight (N : ℕ) (y : T.Node N → K) (b : K)
    (hdiam : ∀ a c : K, ‖(a : X) - c‖ ≤ 1) (s : T.Node N) :
    ‖(E.switchRoot N y b (s.val + 1) : X) - E.switchRoot N y b s.val‖ ≤
      W.pathWeight N s := by
…

def OAI.ReflexiveFixedPoints.TreeEvaluation.switchVector line 78
Source documentation
The normalized difference associated to a single actual leaf switch.
```
noncomputable def switchVector (N : ℕ) (y : T.Node N → K) (b : K)
    (s : T.Node N) : X :=
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchVector_mem_norm_reconstruct line 85

Source documentation

The actual normalized switch vector lies in the whole unit ball of any subspace containing all differences of points in K.

theorem switchVector_mem_norm_reconstruct (N : ℕ) (y : T.Node N → K) (b : K)
    (Y : Submodule ℝ X) (hY : ∀ a c : K, (a : X) - c ∈ Y)
    (hdiam : ∀ a c : K, ‖(a : X) - c‖ ≤ 1) (s : T.Node N) :
    E.switchVector N y b s ∈ Y ∧ ‖E.switchVector N y b s‖ ≤ 1 ∧
      W.pathWeight N s • E.switchVector N y b s =
        (E.switchRoot N y b (s.val + 1) : X) - E.switchRoot N y b s.val := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchRoot_interval_telescope line 98

Source documentation

Consecutive actual root outputs telescope over a half-open interval. No node map is moved through the sum.

theorem switchRoot_interval_telescope (N : ℕ) (y : T.Node N → K) (b : K)
    {lo hi : ℕ} (h : lo ≤ hi) :
    (∑ i ∈ Finset.Ico lo hi,
      ((E.switchRoot N y b (i + 1) : X) - E.switchRoot N y b i)) =
        (E.switchRoot N y b hi : X) - E.switchRoot N y b lo := by
…