CandidateStages.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

The actual recursively constructed infinite frontier tower

A stage is an already constructed finite frontier with its chronological candidate counter and the actual ancestor maps. The next stage is obtained by the concrete finite parent selections. No infinite tree, future detector, or future coefficient is supplied to this recursion.

def OAI.ReflexiveFixedPoints.CandidateContext.runTolerance line 33
Source documentation
A conservative positive tolerance using the complete candidate counter. Its comparison with the retained-budget tolerance is proved separately after the global labels are extracted.
```
def runTolerance : ℝ := (1 / 2 : ℝ) ^ C.depth * candidateBudget C.base
```
Mentions: OAI.ReflexiveFixedPoints.candidateBudget
theorem OAI.ReflexiveFixedPoints.CandidateContext.runTolerance_pos line 35
def OAI.ReflexiveFixedPoints.CandidateContext.selectedExtension line 42
Source documentation
The actual extension used at this stage.
```
def selectedExtension : FrontierExtension C.frontier :=
…
```
Mentions: OAI.ReflexiveFixedPoints.FrontierExtension
def OAI.ReflexiveFixedPoints.CandidateContext.candidateCount line 46
Source documentation
Candidate counts include every map chosen before zero coefficients are removed.
```
def candidateCount : ℕ :=
…
```
theorem OAI.ReflexiveFixedPoints.CandidateContext.candidateCount_pos line 49
def OAI.ReflexiveFixedPoints.CandidateContext.advance line 55
Source documentation
Advance to the next finite frontier using only the completed choices.
```
def advance : CandidateContext D where
…
```
Mentions: OAI.ReflexiveFixedPoints.CandidateContext
theorem OAI.ReflexiveFixedPoints.CandidateContext.advance_frontier line 68
theorem OAI.ReflexiveFixedPoints.CandidateContext.advance_anchor line 71
theorem OAI.ReflexiveFixedPoints.CandidateContext.advance_terminal line 73
theorem OAI.ReflexiveFixedPoints.CandidateContext.advance_ultrafilter line 75
theorem OAI.ReflexiveFixedPoints.CandidateContext.advance_depth line 77
theorem OAI.ReflexiveFixedPoints.CandidateContext.advance_base line 79
theorem OAI.ReflexiveFixedPoints.CandidateContext.advance_ancestors line 82
abbrev OAI.ReflexiveFixedPoints.AnchoredCandidateContext line 91
Source documentation
An actual stage remembers that its anchor is the one selected initially.
```
abbrev AnchoredCandidateContext (D : NormalizedMinimalData (X := X))
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.initial line 102
Source documentation
The initial frontier consists solely of the identity map at the root.
```
def initial : AnchoredCandidateContext D A :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.next line 115
Source documentation
One concrete finite stage, with the original anchor preserved.
```
def next (S : AnchoredCandidateContext D A) : AnchoredCandidateContext D A :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.stages line 119
Source documentation
Ordinary natural recursion constructs all finite levels successively.
```
def stages : ℕ → AnchoredCandidateContext D A
  | 0 => initial D A U
  | k + 1 => next D A (stages k)
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.initial, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.next
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.stages_zero line 123
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.stages_succ line 125
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context line 128
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_anchor line 130
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_succ line 133
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_depth line 137
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_terminal line 144
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_ultrafilter line 151
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_base_zero line 156
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_base_succ line 158
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower line 163
Source documentation
The infinite evaluated tree is extracted only after the finite recursion.
```
def tower : FrontierTower D.K where
…
```
Mentions: OAI.ReflexiveFixedPoints.FrontierTower
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower_frontier line 171
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower_step line 174
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower_generated line 179
Source documentation
All maps of the resulting tree retain their concrete generated origin.
```
theorem tower_generated (k : ℕ) (v : (tower D A U).toOrderedTree.Node k) :
    Generated D.closed D.convex D.T D.nonexpansive
      ((tower D A U).toEvaluation.map k v) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.Generated
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower_childAverage_near line 185
Source documentation
The parent return was proved for the actual new child outputs.
```
theorem tower_childAverage_near (k : ℕ)
    (p : (tower D A U).toOrderedTree.Node k) :
    ‖((tower D A U).toEvaluation.childAverage k
      (fun v => (tower D A U).toEvaluation.map (k + 1) v A.x) p : X) - (A.x : X)‖ <
        (context D A U k).runTolerance := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context