FeasibleBranch.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

A feasible branch with finite prefix witnesses

Feasibility is an existential proposition on a finite node, so the feasible nodes at each level still form a finite type. Restriction to an ancestor preserves the same witness. The elementary graded form of König's lemma then yields one coherent branch, with a witness for every finite prefix.

The witness set is arbitrary. In the fixed-point argument it is instantiated with the whole unit ball of the closed difference span. No compactness or surjectivity of projections between feasible levels is used here.

def OAI.ReflexiveFixedPoints.OrderedTree.DetectsPrefix line 26
Source documentation
One witness satisfies every nonroot detector on the path to a node.
```
def DetectsPrefix (f : (k : ℕ) → T.Node k → D → ℝ)
    {n : ℕ} (v : T.Node n) (d : D) : Prop :=
…
```
def OAI.ReflexiveFixedPoints.OrderedTree.Feasible line 32
Source documentation
Feasibility retains membership in the given witness set.
```
def Feasible (B : Set D) (f : (k : ℕ) → T.Node k → D → ℝ)
    {n : ℕ} (v : T.Node n) : Prop :=
…
```
abbrev OAI.ReflexiveFixedPoints.OrderedTree.FeasibleNode line 37
Source documentation
A feasible node contains only a node and a proposition, not extra witness data.
```
abbrev FeasibleNode (B : Set D) (f : (k : ℕ) → T.Node k → D → ℝ)
    (n : ℕ) :=
…
```
def OAI.ReflexiveFixedPoints.OrderedTree.IsBranch line 42
Source documentation
All earlier coordinates of a branch are the actual ancestors.
```
def IsBranch (b : (n : ℕ) → T.Node n) : Prop :=
…
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.detectsPrefix_zero line 47
theorem OAI.ReflexiveFixedPoints.OrderedTree.feasible_zero line 52

theorem OAI.ReflexiveFixedPoints.OrderedTree.detectsPrefix_ancestorLE line 58

Source documentation

Ancestor restriction keeps the original witness and every earlier constraint.

theorem detectsPrefix_ancestorLE {i j : ℕ} (hij : i ≤ j)
    {v : T.Node j} {d : D} (hd : T.DetectsPrefix f v d) :
    T.DetectsPrefix f (T.ancestorLE hij v) d := by
…

theorem OAI.ReflexiveFixedPoints.OrderedTree.feasible_ancestorLE line 65

theorem OAI.ReflexiveFixedPoints.OrderedTree.exists_feasible_branch line 72

Source documentation

A feasible node at every depth yields a coherent feasible branch.

theorem exists_feasible_branch
    (hne : ∀ n, ∃ v : T.Node n, T.Feasible B f v) :
    ∃ b : (n : ℕ) → T.Node n,
      T.IsBranch b ∧ ∀ n, T.Feasible B f (b n) := by
…

theorem OAI.ReflexiveFixedPoints.OrderedTree.exists_feasible_branch_with_witnesses line 101

Source documentation

Prefix feasibility written directly in the coherent branch coordinates.

theorem exists_feasible_branch_with_witnesses
    (hne : ∀ n, ∃ v : T.Node n, T.Feasible B f v) :
    ∃ b : (n : ℕ) → T.Node n,
      T.IsBranch b ∧
      ∀ n, ∃ d ∈ B, ∀ i, 0 < i → i ≤ n →
        (1 / 2 : ℝ) ≤ f i (b i) d := by
…

theorem OAI.ReflexiveFixedPoints.OrderedTree.exists_branch_of_finite_witnesses line 118

Source documentation

The positive-depth finite witness theorem suffices; depth zero uses any element of B.

theorem exists_branch_of_finite_witnesses (hB : B.Nonempty)
    (hfinite : ∀ n, 0 < n → ∃ v : T.Node n,
      ∃ d ∈ B, T.DetectsPrefix f v d) :
    ∃ b : (n : ℕ) → T.Node n,
      T.IsBranch b ∧
      ∀ n, ∃ d ∈ B, ∀ i, 0 < i → i ≤ n →
        (1 / 2 : ℝ) ≤ f i (b i) d := by
…

theorem OAI.ReflexiveFixedPoints.OrderedTree.IsBranch.root_eq line 131
theorem OAI.ReflexiveFixedPoints.OrderedTree.IsBranch.parent_eq line 135