FiniteWitness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A common path witness from actual block detection

Every vector in this finite argument is the normalized increment of the same actual right-to-left switching experiment. The construction of the terminal point and the proof of block detection are supplied by the later tree-data integration; they are not assumptions of the final fixed-point theorem.

abbrev OAI.ReflexiveFixedPoints.OrderedTree.TruncationNode line 24
Source documentation
All nonroot nodes in a finite truncation, with their actual finite levels.
```
abbrev TruncationNode (T : OrderedTree) (N : ℕ) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree
theorem OAI.ReflexiveFixedPoints.OrderedTree.TruncationNode.levelBound line 31

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.finite_witness_of_block_detection line 46

Source documentation

Actual before/after block detection yields one leaf whose own normalized root increment is detected at every nonroot point of its ancestor path. There is no lower bound on the positive path weights.

theorem finite_witness_of_block_detection
    (N : ℕ) (y : T.Node N → K) (b : K)
    (Y : Submodule ℝ X) (hY : ∀ a c : K, (a : X) - c ∈ Y)
    (hdiam : ∀ a c : K, ‖(a : X) - c‖ ≤ 1)
    (f : (k : ℕ) → T.Node k → X →L[ℝ] ℝ)
    (hf : ∀ k v, ‖f k v‖ ≤ 1)
    (e : T.TruncationNode N → ℝ)
    (he : (∑ v, e v) ≤ (1 : ℝ) / 128)
    (hblock : ∀ v : T.TruncationNode N,
      W.pathWeight (v.1.val + 1) v.2 - 5 * e v ≤
        f (v.1.val + 1) v.2
          ((E.beforeBlock v.levelBound y b v.2 : X) -
…