OrderedRoutePreservation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.OrderedRoutePreservation.routingChoice line 17
Source documentation
The node-choice function induced by ordered selector tables.
```
def routingChoice (S : List (Fin (M + 1)) → X → Fin M → Bool) :
    List (Fin (M + 1)) → X → Fin (M + 1) :=
…
```

theorem OAI.Problem310.OrderedRoutePreservation.preserved_prefix line 23

Source documentation

Agreement of exactly the selector entries queried along a nondefault center path preserves its common prefix. Later siblings need not agree.

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

Mentions: OAI.Problem310.OrderedRoutePreservation.routingChoice

theorem OAI.Problem310.OrderedRoutePreservation.child_of_default_local_success line 48

Source documentation

At a default center node, stable earlier sibling selectors remain rejected, so the successful local selector chooses the tested child.

theorem child_of_default_local_success
    (S : List (Fin (M + 1)) → X → Fin M → Bool)
    (U : List (Fin (M + 1))) (x y : X) (i : Fin M)
    (hdefault : routingChoice S U x = Fin.last M)
    (hstable : ∀ j < i, S U x j = S U y j)
    (hsuccess : S U y i = true) : routingChoice S U y = i.castSucc := by
…

Mentions: OAI.Problem310.OrderedRoutePreservation.routingChoice

theorem OAI.Problem310.OrderedRoutePreservation.terminal_success_of_stable_local_test line 62

Source documentation

The full deterministic route-preservation implication of the random routing construction, independent of the numerical grid and probability implementations.

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

Mentions: OAI.Problem310.OrderedRoutePreservation.routingChoice