WindowExceptionalTransfer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem310.WindowExceptionalTransfer.local_depth line 16
def OAI.Problem310.WindowExceptionalTransfer.localQ line 23
Source documentation
The actual local Boolean test, using the canonical tables and subtree router.
```
def localQ (W : WindowData (M + 1) d g r₀) (U : Node M d)
    (ω : SelectorTable (selectorEndpoints W) × TerminalTable (terminalEndpoints W))
    (i : Fin M) (y : ℝ) : Bool :=
…
```
Mentions: OAI.Problem310.WindowData
def OAI.Problem310.WindowExceptionalTransfer.StableAt line 33
Source documentation
Stability in precisely the selector-value form supplied by the canonical window stability construction.
```
def StableAt (W : WindowData (M + 1) d g r₀) (x : ℝ) : Prop :=
…
```
Mentions: OAI.Problem310.WindowData
lemma OAI.Problem310.WindowExceptionalTransfer.localQ_mem_routedSet line 40

theorem OAI.Problem310.WindowExceptionalTransfer.exists_representatives_failure_transfer line 74

Source documentation

Raw exceptional failure on a fixed good center atom transfers to one finite representative scale at which every actual local Boolean trial fails.

theorem exists_representatives_failure_transfer
    (W : WindowData (M + 1) d g r₀) (U : Node M d) (k : ℕ) (x : ℝ)
    (ξ : Node M d × Fin M → Bool)
    (hfirst : ∀ ω : SelectorTable (selectorEndpoints W),
      centerExposure (selectorEndpoints W) x ω = ξ →
      routeFrom (selectorChoice (selectorEndpoints W) ω) k [] x = U.val ∧
      selectorChoice (selectorEndpoints W) ω U.val x = Fin.last M ∧
      ∀ l < k, selectorChoice (selectorEndpoints W) ω
        (routeFrom (selectorChoice (selectorEndpoints W) ω) l [] x) x ≠ Fin.last M)
    (hstable : StableAt W x) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc (1 : ℝ) 2) ∧
…

Mentions: OAI.Problem310.WindowData, OAI.Problem310.WindowExceptionalTransfer.StableAt