RoutedExposure.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.RoutedExposure.selectorChoice_eq_centerChoice line 11

theorem OAI.Problem310.RoutedExposure.routedPath_eq_centerRoute line 18

Source documentation

Translate from spatial routing with tables fixed to routing the table outcome with the center fixed. No decision or node representation is changed.

theorem routedPath_eq_centerRoute {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (ω : SelectorTable b) (x : ℝ)
    (n : ℕ) (P : List (Child M)) :
    routeFrom (selectorChoice b ω) n P x = routeFrom (centerChoice b x) n P ω :=
…

theorem OAI.Problem310.RoutedExposure.routedLeaf_eq_of_centerExposure_eq line 25

Source documentation

The actual finite terminal leaf at the center is fixed on each exposure atom.

theorem routedLeaf_eq_of_centerExposure_eq {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) {ω ω' : SelectorTable b}
    (h : centerExposure b x ω = centerExposure b x ω') :
    routedLeaf b ω x = routedLeaf b ω' x := by
…

theorem OAI.Problem310.RoutedExposure.routedAddress_eq_of_centerExposure_eq line 35

Source documentation

Therefore the actual terminal table address at the center is fixed as well.

theorem routedAddress_eq_of_centerExposure_eq {M d : ℕ}
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ) (x : ℝ)
    {ω ω' : SelectorTable bS} (h : centerExposure bS x ω = centerExposure bS x ω') :
    routedAddress bS bT ω x = routedAddress bS bT ω' x := by
…

theorem OAI.Problem310.RoutedExposure.badExposure_iff_actual_no_default line 43

Source documentation

The bad-exposure event in the atom average is exactly the actual raw router's no-default event, in the notation of RoutedSetDensity.

theorem badExposure_iff_actual_no_default {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) (ω : SelectorTable b) :
    ¬ GoodExposure b x (centerExposure b x ω) ↔
      ∀ k < d, selectorChoice b ω (routeFrom (selectorChoice b ω) k [] x) x ≠ Fin.last M := by
…

theorem OAI.Problem310.RoutedExposure.actual_firstDefaultNode_on_atom line 52

Source documentation

A good exposure supplies the actual bounded first-default node, fixed before any remaining selector or terminal-table coordinates are revealed.

theorem actual_firstDefaultNode_on_atom {M d : ℕ}
    (b : Node M d → Fin M → ℕ) (x : ℝ) (ξ : Node M d × Fin M → Bool)
    (hgood : GoodExposure b x ξ) :
    ∃ k : Fin d, ∃ U : Node M d, U.val.length = k.val ∧
      ∀ ω : SelectorTable b, centerExposure b x ω = ξ →
        routeFrom (selectorChoice b ω) k.val [] x = U.val ∧
        selectorChoice b ω U.val x = Fin.last M ∧
        ∀ l < k.val,
          selectorChoice b ω (routeFrom (selectorChoice b ω) l [] x) x ≠ Fin.last M := by
…