SwitchingBlocks.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual whole-block switches and their vector telescope

The ordered descendant interval determines the actual before/after root states. All leaf increments come from the same cutoff experiment.

theorem OAI.ReflexiveFixedPoints.OrderedTree.sum_descendants_eq_Ico line 23

Source documentation

Reindex a sum over an actual descendant fiber by its consecutive natural interval.

theorem sum_descendants_eq_Ico (T : OrderedTree)
    {k N : ℕ} (h : k ≤ N) (v : T.Node k)
    {A : Type*} [AddCommMonoid A] (f : ℕ → A) :
    (∑ s ∈ T.descendants h v, f s.val) =
      ∑ i ∈ Finset.Ico (T.descendantLo h v) (T.descendantHi h v), f i := by
…

Mentions: OAI.ReflexiveFixedPoints.OrderedTree

def OAI.ReflexiveFixedPoints.TreeEvaluation.beforeBlock line 53
Source documentation
The actual root just before the entire descendant block switches.
```
noncomputable def beforeBlock {k N : ℕ} (h : k ≤ N)
    (y : T.Node N → K) (b : K) (v : T.Node k) : K :=
…
```
def OAI.ReflexiveFixedPoints.TreeEvaluation.afterBlock line 58
Source documentation
The actual root just after the entire descendant block switches.
```
noncomputable def afterBlock {k N : ℕ} (h : k ≤ N)
    (y : T.Node N → K) (b : K) (v : T.Node k) : K :=
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchLeaves_beforeBlock line 64

Source documentation

At the before-block cutoff, a leaf is unchanged exactly when its depth-k ancestor is at or to the left of the block's node.

theorem switchLeaves_beforeBlock {k N : ℕ} (h : k ≤ N)
    (y : T.Node N → K) (b : K) (v : T.Node k) (s : T.Node N) :
    E.switchLeaves N y b (T.descendantHi h v) s =
      if T.ancestorLE h s ≤ v then y s else b := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchLeaves_afterBlock line 72

Source documentation

At the after-block cutoff, a leaf is unchanged exactly when its depth-k ancestor is strictly to the left of the block's node.

theorem switchLeaves_afterBlock {k N : ℕ} (h : k ≤ N)
    (y : T.Node N → K) (b : K) (v : T.Node k) (s : T.Node N) :
    E.switchLeaves N y b (T.descendantLo h v) s =
      if T.ancestorLE h s < v then y s else b := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.switchLeaves_beforeBlock_of_descendant line 79

Source documentation

A node's own descendants are all unchanged immediately before its block.

theorem switchLeaves_beforeBlock_of_descendant {k N : ℕ} (h : k ≤ N)
    (y : T.Node N → K) (b : K) (v : T.Node k) (s : T.Node N)
    (hs : T.ancestorLE h s = v) :
    E.switchLeaves N y b (T.descendantHi h v) s = y s := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.pathWeight_smul_switchVector line 87
Source documentation
Multiplying the actual normalized increment by its positive path weight recovers exactly the actual before-minus-after single-leaf difference.
```
theorem pathWeight_smul_switchVector (N : ℕ) (y : T.Node N → K) (b : K)
    (s : T.Node N) :
    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.switchVector_block_telescope line 96

Source documentation

The sum of the actual normalized leaf increments over a descendant block is exactly its actual before-minus-after root difference.

theorem switchVector_block_telescope {k N : ℕ} (h : k ≤ N)
    (y : T.Node N → K) (b : K) (v : T.Node k) :
    (∑ s ∈ T.descendants h v, W.pathWeight N s • E.switchVector N y b s) =
      (E.beforeBlock h y b v : X) - E.afterBlock h y b v := by
…