FiniteLocalPredicate.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.FiniteLocalPredicate.localLeaf line 15

Source documentation

The leaf reached from a local child, with its ambient-depth proof retained.

def localLeaf (choose : List (Child M) → ℝ → Child M)
    (r : ℕ) (P : List (Child M)) (hdepth : P.length + r = d) (x : ℝ) : Leaf M d :=
…

theorem OAI.Problem310.FiniteLocalPredicate.selector_lookup_eq line 20

Source documentation

Table lookup at a valid node depends only on a finer common grid.

theorem selector_lookup_eq {b : Node M d → Fin M → ℕ} (ω : SelectorTable b)
    (Q : Node M d) (i : Fin M) {B : ℕ} (hb : b Q i ≤ B) {x y : ℝ}
    (hxy : ⌊(2 : ℝ) ^ (B + 2) * Int.fract x⌋ =
      ⌊(2 : ℝ) ^ (B + 2) * Int.fract y⌋) :
    ω (selectorAddress b Q i x) = ω (selectorAddress b Q i y) := by
…

theorem OAI.Problem310.FiniteLocalPredicate.terminal_lookup_eq line 28

Source documentation

The analogous statement for an actual dependent terminal-table address.

theorem terminal_lookup_eq {b : Leaf M d → ℕ} (ω : TerminalTable b)
    (L : Leaf M d) {B : ℕ} (hb : b L ≤ B) {x y : ℝ}
    (hxy : ⌊(2 : ℝ) ^ (B + 2) * Int.fract x⌋ =
      ⌊(2 : ℝ) ^ (B + 2) * Int.fract y⌋) :
    ω (terminalAddress b L x) = ω (terminalAddress b L y) := by
…

theorem OAI.Problem310.FiniteLocalPredicate.finite_local_predicate_factors line 38

Source documentation

Concrete local terminal predicates in the finite table model factor through the largest resolution in the child subtree. rule may be the canonical first-success/default rule; no assumptions on that rule are needed.

theorem finite_local_predicate_factors
    (bS : Node M d → Fin M → ℕ) (bT : Leaf M d → ℕ)
    (ωS : SelectorTable bS) (ωT : TerminalTable bT)
    (choose : List (Child M) → ℝ → Child M)
    (rule : List (Child M) → (Fin M → Bool) → Child M)
    (hchoose : ∀ Q x, choose Q x = rule Q (fun i => selectorValue bS ωS Q i x))
    (r : ℕ) (P : List (Child M)) (hdepth : P.length + r = d)
    (U : Node M d) (i : Fin M) (B : ℕ)
    (hbS : ∀ Q : Node M d, P.IsPrefix Q.val → ∀ j, bS Q j ≤ B)
    (hbT : ∀ L : Leaf M d, P.IsPrefix L.val → bT L ≤ B)
    (hIn : bS U i ≤ B) {x y : ℝ}
    (hxy : ⌊(2 : ℝ) ^ (B + 2) * Int.fract x⌋ =
…