StableRoutingBridge.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.StableRouting.select line 17
Source documentation
Ordered routing associated to the spatial selector values.
```
def select (S : List (Fin (M + 1)) → Fin M → X → Bool)
    (P : List (Fin (M + 1))) (x : X) : Fin (M + 1) :=
…
```

theorem OAI.Problem310.StableRouting.select_eq_of_earlier_agreement line 22

Source documentation

A nondefault decision is unchanged if all selectors up to that decision agree.

theorem select_eq_of_earlier_agreement
    (S : List (Fin (M + 1)) → Fin M → X → Bool)
    (P : List (Fin (M + 1))) (x y : X)
    (hnd : select S P x ≠ Fin.last M)
    (hagree : ∀ j : Fin M, j.castSucc ≤ select S P x → S P j x = S P j y) :
    select S P y = select S P x := by
…

Mentions: OAI.Problem310.StableRouting.select

theorem OAI.Problem310.StableRouting.route_eq_of_earlier_selector_agreement line 36

Source documentation

Stable earlier selector addresses preserve the path before its first default.

theorem route_eq_of_earlier_selector_agreement
    (S : List (Fin (M + 1)) → Fin M → X → Bool)
    (k : ℕ) (P : List (Fin (M + 1))) (x y : X)
    (hnd : ∀ l < k, select S (routeFrom (select S) l P x) x ≠ Fin.last M)
    (hagree : ∀ l < k, ∀ j : Fin M,
      j.castSucc ≤ select S (routeFrom (select S) l P x) x →
      S (routeFrom (select S) l P x) j x = S (routeFrom (select S) l P x) j y) :
    routeFrom (select S) k P y = routeFrom (select S) k P x := by
…

Mentions: OAI.Problem310.StableRouting.select

theorem OAI.Problem310.StableRouting.rejects_earlier_at_default line 49

Source documentation

At a center's default node, preserving the earlier selectors rejects those children.

theorem rejects_earlier_at_default
    (S : List (Fin (M + 1)) → Fin M → X → Bool)
    (U : List (Fin (M + 1))) (x y : X) (i : Fin M)
    (hdefault : select S U x = Fin.last M)
    (hagree : ∀ j < i, S U j x = S U j y) :
    ∀ j < i, S U j y = false := by
…

Mentions: OAI.Problem310.StableRouting.select

theorem OAI.Problem310.StableRouting.terminal_success_of_stable_local_success line 61

Source documentation

The local-hit implication, with its geometric input isolated as selector agreement. Later sibling selectors and off-prefix choices are unrestricted.

theorem terminal_success_of_stable_local_success
    (S : List (Fin (M + 1)) → Fin M → X → Bool)
    (terminal : List (Fin (M + 1)) → X → Prop)
    (k r : ℕ) (P U : List (Fin (M + 1))) (x y : X) (i : Fin M)
    (hU : routeFrom (select S) k P x = U)
    (hnd : ∀ l < k, select S (routeFrom (select S) l P x) x ≠ Fin.last M)
    (hprefix : ∀ l < k, ∀ j : Fin M,
      j.castSucc ≤ select S (routeFrom (select S) l P x) x →
      S (routeFrom (select S) l P x) j x = S (routeFrom (select S) l P x) j y)
    (hdefault : select S U x = Fin.last M)
    (hearlier : ∀ j < i, S U j x = S U j y)
    (hi : S U i y = true)
…

Mentions: OAI.Problem310.StableRouting.select