TreeFiniteWitness.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite witnesses from the actual constructed tree

The construction discharges the terminal, subtree, path, detector, and weighted budget hypotheses of the finite switching argument using the actual tree data. It keeps the chosen vector in the entire original-norm difference ball.

def OAI.ReflexiveFixedPoints.SwitchingTreeData.truncationEmbedding line 32
Source documentation
Forget the finite level bound without changing a node or its candidate label.
```
def truncationEmbedding (N : ℕ) (v : A.tree.TruncationNode N) : A.tree.NonrootNode :=
…
```
theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.truncationEmbedding_injective line 35
theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.finite_budget_le line 46
Source documentation
Every finite truncation uses its original retained candidate budgets.
```
theorem finite_budget_le (N : ℕ) :
    (∑ v : A.tree.TruncationNode N, A.budget (v.1.val + 1) v.2) ≤
      (1 : ℝ) / 128 := by
…
```

theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.exists_finite_terminal line 55

Source documentation

One actual terminal resolvent satisfies every finite prediction detector and the full displacement sum through the terminal level.

theorem exists_finite_terminal (N : ℕ) :
    ∃ j,
      (∀ v : A.tree.TruncationNode N,
        1 - 2 * A.budget (v.1.val + 1) v.2 ≤
          A.functionalAt (v.1.val + 1) v.2
            ((A.nodeLabel (v.1.val + 1) v.2 : X) -
              A.evaluation.evaluate (v.1.val + 1)
                (A.evaluation.idealCutoff (v.1.val + 1) A.anchor (A.terminal j) v.2))) ∧
      A.evaluation.terminalDefect (N + 1) (A.terminal j) ≤
        A.tree.cumulativeMinimum (OrderedTree.retainedBudget A.label) N := by
…

Mentions: OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget

theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.finite_block_detection line 98

Source documentation

All of the actual finite tree's block detector inequalities hold at the same selected terminal point.

theorem finite_block_detection (N j : ℕ)
    (hdet : ∀ v : A.tree.TruncationNode N,
      1 - 2 * A.budget (v.1.val + 1) v.2 ≤
        A.functionalAt (v.1.val + 1) v.2
          ((A.nodeLabel (v.1.val + 1) v.2 : X) -
            A.evaluation.evaluate (v.1.val + 1)
              (A.evaluation.idealCutoff (v.1.val + 1) A.anchor (A.terminal j) v.2)))
    (hD : A.evaluation.terminalDefect (N + 1) (A.terminal j) ≤
      A.tree.cumulativeMinimum (OrderedTree.retainedBudget A.label) N)
    (v : A.tree.TruncationNode N) :
    A.weights.pathWeight (v.1.val + 1) v.2 - 5 * A.budget (v.1.val + 1) v.2 ≤
      A.functionalAt (v.1.val + 1) v.2
…

Mentions: OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget

theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.difference_mem_span line 128
Source documentation
The actual normalized differences lie in the original difference span.
```
theorem difference_mem_span (_A : SwitchingTreeData D) (a b : D.K) :
    (a : X) - b ∈ differenceSpan D.K := by
…
```
Mentions: OAI.ReflexiveFixedPoints.SwitchingTreeData, OAI.ReflexiveFixedPoints.differenceSpan
theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.finite_witness line 135
Source documentation
The constructed infinite tree has a whole-ball witness at every finite depth. Every central switching estimate has been discharged above.
```
theorem finite_witness (N : ℕ) :
    ∃ v : A.tree.Node N, ∃ d ∈ differenceBall D.K,
      A.tree.DetectsPrefix (fun k v x => A.functionalAt k v x) v d := by
…
```
Mentions: OAI.ReflexiveFixedPoints.differenceBall