TreeProducer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual adaptive ordered tree

The anchor is produced by the resolvent-tail construction. A fixed ultrafilter refines the ordinary tail filter. Concrete finite candidate selections then construct each level, keeping every discarded candidate in its history. The finite-frontier recursion produces the final tree and all its detector, weight, return, path, and ideal-prediction conclusions.

def OAI.ReflexiveFixedPoints.switchingTreeDataOfAnchor line 29
Source documentation
Assemble the proved conclusions of the actual finite-stage recursion.
```
def switchingTreeDataOfAnchor
    (D : NormalizedMinimalData (X := X))
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData
theorem OAI.ReflexiveFixedPoints.exists_switchingTreeData line 57
Source documentation
The tree, its anchor and all central construction laws are produced from the actual normalized minimal invariant set.
```
theorem exists_switchingTreeData (D : NormalizedMinimalData (X := X)) :
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData