CandidatePreparation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Preparing a candidate from the completed history

The actual compact prediction set and all ancestor displacement constants are fixed before selecting a candidate map. Their detector scale and finite sum determine one tail threshold. Every map in that tail then has a detector and satisfies the ancestor displacement budget at every input.

theorem OAI.ReflexiveFixedPoints.exists_prepared_candidate_threshold line 39
Source documentation
Prepare one tail threshold from the existing finite frontier and its earlier outputs. The quantified candidate map and its input occur only after that threshold has been selected. The detector separates the candidate output from every point of the actual compact prediction set, including its prescribed dense prefix.
Each ancestor constant is obtained from its Generated derivation. The same threshold controls their total displacement; no additional geometric assumption or assumed candidate-selection law is used.
```
theorem exists_prepared_candidate_threshold
    (D : NormalizedMinimalData (X := X)) (F : TreeFrontier D.K)
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData, OAI.ReflexiveFixedPoints.TreeFrontier