BranchContradiction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The branch contradiction from the actual finite witnesses

The actual ordered tree supplies detector labels and summable budgets. The finite switching witnesses give a feasible branch. Weak compactness of the whole difference ball keeps one common vector, whereas the same detectors vanish on its closed difference span by density and their uniform norm bound.

theorem OAI.ReflexiveFixedPoints.abs_apply_sub_le_of_detector line 26

Source documentation

Two detector values in the same interval of length e differ by at most e.

theorem abs_apply_sub_le_of_detector (f : X →L[ℝ] ℝ) (hf : ‖f‖ ≤ 1)
    (y a b : X) (e : ℝ)
    (hya : ‖y - a‖ ≤ 1) (hyb : ‖y - b‖ ≤ 1)
    (ha : 1 - e ≤ f (y - a)) (hb : 1 - e ≤ f (y - b)) :
    |f (a - b)| ≤ e := by
…

theorem OAI.ReflexiveFixedPoints.tree_finite_witnesses_contradiction line 46
Source documentation
The precise outputs of the tree and finite switching construction cannot coexist in the normalized minimal data. Every listed input is supplied by an earlier concrete producer; no branch or pointwise-vanishing premise is used.
```
theorem tree_finite_witnesses_contradiction
    (D : NormalizedMinimalData (X := X)) (T : OrderedTree)
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData, OAI.ReflexiveFixedPoints.OrderedTree