FiniteLocalHit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.FiniteLocalHit.local_test_implies_root_hit line 16

Source documentation

A successful concrete child-local test is a successful terminal lookup on the actual root route. Only the earlier center-path selectors must be stable.

theorem local_test_implies_root_hit
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (ωS : SelectorTable bS) (ωT : TerminalTable bT)
    (k r : ℕ) (U : Node M d) (i : Fin M) (x y : ℝ)
    (hdepth : (U.val ++ [i.castSucc]).length + r = d)
    (hU : routeFrom (select (selectorValue bS ωS)) k [] x = U.val)
    (hnd : ∀ l < k, select (selectorValue bS ωS)
      (routeFrom (select (selectorValue bS ωS)) l [] x) x ≠ Fin.last M)
    (hprefix : ∀ l < k, ∀ j : Fin M,
      j.castSucc ≤ select (selectorValue bS ωS)
        (routeFrom (select (selectorValue bS ωS)) l [] x) x →
      selectorValue bS ωS (routeFrom (select (selectorValue bS ωS)) l [] x) j x =
…

theorem OAI.Problem310.FiniteLocalHit.local_test_mem_routedSet line 62

Source documentation

Final canonical-set form of the local-hit implication. This uses precisely the concrete selectorChoice, localLeaf, and routedSet definitions of the model.

theorem local_test_mem_routedSet
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (ωS : SelectorTable bS) (ωT : TerminalTable bT)
    (k r : ℕ) (U : Node M d) (i : Fin M) (x y : ℝ)
    (hdepth : (U.val ++ [i.castSucc]).length + r = d)
    (hU : routeFrom (RoutedSetDensity.selectorChoice bS ωS) k [] x = U.val)
    (hnd : ∀ l < k, RoutedSetDensity.selectorChoice bS ωS
      (routeFrom (RoutedSetDensity.selectorChoice bS ωS) l [] x) x ≠ Fin.last M)
    (hprefix : ∀ l < k, ∀ j : Fin M,
      j.castSucc ≤ RoutedSetDensity.selectorChoice bS ωS
        (routeFrom (RoutedSetDensity.selectorChoice bS ωS) l [] x) x →
      selectorValue bS ωS (routeFrom (RoutedSetDensity.selectorChoice bS ωS) l [] x) j x =
…

Mentions: OAI.Problem310.RoutedSetDensity.selectorChoice