NormalizedContradiction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual tree and switching contradiction for normalized minimal data

The adaptive producer constructs the tree without an added geometric premise. Its actual finite switching witnesses lie in the whole difference ball, and the branch argument contradicts the produced dense-point detectors there.

theorem OAI.ReflexiveFixedPoints.SwitchingTreeData.contradiction line 24
Source documentation
The concrete constructed tree cannot coexist with normalized minimal data.
```
theorem contradiction {D : NormalizedMinimalData (X := X)} (A : SwitchingTreeData D) :
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData, OAI.ReflexiveFixedPoints.SwitchingTreeData
theorem OAI.ReflexiveFixedPoints.normalizedMinimalData_false line 41
Source documentation
No normalized minimal invariant counterexample exists. This calls the actual adaptive-tree producer and the fully discharged finite switching proof.
```
theorem normalizedMinimalData_false (D : NormalizedMinimalData (X := X)) : False := by
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData