CandidateSelection.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Actual adaptive selection of one parent's candidate group

Every state carries a valid complete candidate history. Its threshold is computed from that history before the next map is chosen. The actual compact detector then produces a legal new record. The adaptive anchor chooses a finite return, and only afterward does positive-support extraction select its children. Neither candidate existence nor a return law is assumed.

abbrev OAI.ReflexiveFixedPoints.CandidateContext.State line 35
Source documentation
The type used by adaptive selection contains only valid immutable histories.
```
abbrev State := HistoryState (CandidateRecord C) C.Legal
```
Mentions: OAI.ReflexiveFixedPoints.HistoryState, OAI.ReflexiveFixedPoints.CandidateRecord
theorem OAI.ReflexiveFixedPoints.CandidateContext.exists_threshold line 39
Source documentation
A threshold prepared solely from the existing history works for every map in its actual resolvent tail. Auxiliary records are selected afterward.
```
theorem exists_threshold (p : Fin C.frontier.size)
    (history : List (CandidateRecord C)) :
    ∃ m : ℕ, 1 ≤ m ∧ ∀ g : D.K → D.K,
      g ∈ tailFamily D.closed D.convex D.T D.nonexpansive m →
      ∃ r : CandidateRecord C, r.parent = p ∧ r.map = g ∧ C.Legal history r := by
…
```
Mentions: OAI.ReflexiveFixedPoints.CandidateRecord, OAI.ReflexiveFixedPoints.tailFamily
def OAI.ReflexiveFixedPoints.CandidateContext.threshold line 54
Source documentation
No selected map or convex coefficient is an argument to this threshold.
```
def threshold (p : Fin C.frontier.size) (_i : ℕ) (s : C.State) : ℕ :=
…
```
theorem OAI.ReflexiveFixedPoints.CandidateContext.threshold_pos line 57
def OAI.ReflexiveFixedPoints.CandidateContext.Transition line 62
Source documentation
One transition appends exactly one actual selected map and its detector.
```
def Transition (p : Fin C.frontier.size) (_i : ℕ)
    (s : C.State) (g : D.K → D.K) (s' : C.State) : Prop :=
…
```

theorem OAI.ReflexiveFixedPoints.CandidateContext.exists_transition line 68

Source documentation

Post-map auxiliary selection is total on the valid state type.

theorem exists_transition (p : Fin C.frontier.size) (i : ℕ) (s : C.State)
    (g : D.K → D.K)
    (hg : g ∈ tailFamily D.closed D.convex D.T D.nonexpansive (C.threshold p i s)) :
    ∃ s', C.Transition p i s g s' := by
…

Mentions: OAI.ReflexiveFixedPoints.tailFamily

theorem OAI.ReflexiveFixedPoints.CandidateContext.transition_length line 76

theorem OAI.ReflexiveFixedPoints.CandidateContext.transition_take line 83

Source documentation

Earlier entries survive a legal transition literally.

theorem transition_take {p : Fin C.frontier.size} {i : ℕ} {s s' : C.State}
    {g : D.K → D.K} (h : C.Transition p i s g s') :
    s'.entries.take s.entries.length = s.entries := by
…

abbrev OAI.ReflexiveFixedPoints.CandidateContext.ParentReturn line 92
Source documentation
Every parent return retains the full states and candidates, including candidates subsequently assigned coefficient zero.
```
abbrev ParentReturn (p : Fin C.frontier.size) (initial : C.State) (τ : ℝ) :=
…
```
def OAI.ReflexiveFixedPoints.CandidateContext.selectParent line 98
Source documentation
The actual anchor discharges all analytic inputs to adaptive selection.
```
def selectParent
    (A : AnchorPoint (tailFamily D.closed D.convex D.T D.nonexpansive))
    (hanchor : C.anchor = A.x) (p : Fin C.frontier.size)
    (initial : C.State) {τ : ℝ} (hτ : 0 < τ) : C.ParentReturn p initial τ := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchorPoint, OAI.ReflexiveFixedPoints.tailFamily