OrderedRouting.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.OrderedRouting.chooseChild line 8
Source documentation
The first successful nondefault selector, or the final (default) child.
```
def chooseChild {M : ℕ} (S : Fin M → Bool) : Fin (M + 1) :=
…
```
theorem OAI.Problem310.OrderedRouting.chooseChild_eq_nondefault_iff line 13
theorem OAI.Problem310.OrderedRouting.chooseChild_eq_default_iff line 30
theorem OAI.Problem310.OrderedRouting.chooseChild_preserved line 44
Source documentation
Routing to a nondefault child depends only on selector entries up to it.
```
theorem chooseChild_preserved (S T : Fin M → Bool) (i : Fin M)
    (hS : chooseChild S = i.castSucc) (heq : ∀ j ≤ i, S j = T j) :
    chooseChild T = i.castSucc := by
…
```
Mentions: OAI.Problem310.OrderedRouting.chooseChild
theorem OAI.Problem310.OrderedRouting.chooseChild_of_local_success line 57
Source documentation
Rejected earlier children and a successful current selector determine a hit.
```
theorem chooseChild_of_local_success (S : Fin M → Bool) (i : Fin M)
    (hprev : ∀ j < i, S j = false) (hi : S i = true) :
    chooseChild S = i.castSucc :=
…
```
Mentions: OAI.Problem310.OrderedRouting.chooseChild
theorem OAI.Problem310.OrderedRouting.chooseChild_reject_before line 63
Source documentation
Every nondefault child preceding the chosen child was rejected.
```
theorem chooseChild_reject_before (S : Fin M → Bool) (j : Fin M)
    (hj : j.castSucc < chooseChild S) : S j = false := by
…
```
Mentions: OAI.Problem310.OrderedRouting.chooseChild
theorem OAI.Problem310.OrderedRouting.chooseChild_success line 70
Source documentation
A nondefault chosen child has a successful selector.
```
theorem chooseChild_success (S : Fin M → Bool) (i : Fin M)
    (hi : chooseChild S = i.castSucc) : S i = true :=
…
```
Mentions: OAI.Problem310.OrderedRouting.chooseChild
theorem OAI.Problem310.OrderedRouting.chooseChild_ne_default_iff line 75
Source documentation
The default is avoided exactly when some nondefault selector succeeds.
```
theorem chooseChild_ne_default_iff (S : Fin M → Bool) :
    chooseChild S ≠ Fin.last M ↔ ∃ i, S i = true := by
…
```
Mentions: OAI.Problem310.OrderedRouting.chooseChild
theorem OAI.Problem310.OrderedRouting.chooseChild_congr line 81
Source documentation
Pointwise equality of selectors preserves the complete child choice.
```
theorem chooseChild_congr (S T : Fin M → Bool) (h : ∀ i, S i = T i) :
    chooseChild S = chooseChild T := by
…
```
Mentions: OAI.Problem310.OrderedRouting.chooseChild