AdaptiveParentReturn.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite parent returns with their full adaptive history

The finite return is obtained from adaptive_finite_selection. Its full candidate list and all successive states remain available, including the candidates of coefficient zero. A separate order embedding identifies exactly the positive coefficients used as retained children.

theorem OAI.ReflexiveFixedPoints.positive_support_reindex_exact line 26

Source documentation

Ordered positive-support extraction, including its exact range.

theorem positive_support_reindex_exact {N : ℕ}
    (u : Fin N → X) (β : Fin N → ℝ)
    (hβ : ∀ i, 0 ≤ β i) (hβ1 : ∑ i, β i = 1) :
    ∃ (q : ℕ), 0 < q ∧ ∃ (e : Fin q ↪o Fin N),
      (∀ j, 0 < β (e j)) ∧ (∑ j, β (e j) = 1) ∧
      ((∑ j, β (e j) • u (e j)) = ∑ i, β i • u i) ∧
      ∀ i, (∃ j, e j = i) ↔ 0 < β i := by
…

structure OAI.ReflexiveFixedPoints.AdaptiveParentReturn line 67
Source documentation
A finite return to one parent. state and selected describe the entire legal sequence. retain extracts exactly its positive coefficients in the original order, without discarding any of the stored transitions.
```
structure AdaptiveParentReturn {K : Set X} {M : Type v} {S : Type w}
    (eval : M → K) (family : ℕ → Set M) (x : K)
    (threshold : ℕ → S → ℕ)
    (transition : ℕ → S → M → S → Prop) (initial : S) (τ : ℝ) where
…
```

theorem OAI.ReflexiveFixedPoints.AdaptiveParentReturn.retained_near line 94

Source documentation

The retained children have the same return estimate as the full sequence.

theorem AdaptiveParentReturn.retained_near
    {K : Set X} {M : Type v} {S : Type w}
    {eval : M → K} {family : ℕ → Set M} {x : K}
    {threshold : ℕ → S → ℕ}
    {transition : ℕ → S → M → S → Prop} {initial : S} {τ : ℝ}
    (r : AdaptiveParentReturn eval family x threshold transition initial τ) :
    ‖(∑ j, r.β (r.retain j) • (eval (r.selected (r.retain j)) : X)) -
      (x : X)‖ < τ := by
…

Mentions: OAI.ReflexiveFixedPoints.AdaptiveParentReturn

theorem OAI.ReflexiveFixedPoints.adaptive_parent_return_nonempty line 107

Source documentation

Actual finite parent returns exist by adaptive finite selection and ordered support extraction; no finite-return law is assumed.

theorem adaptive_parent_return_nonempty
    {K : Set X} [TopologicalSpace.MetrizableSpace (WeakCarrier K)]
    {M : Type v} {S : Type w}
    (eval : M → K) (family : ℕ → Set M) (x : K) (D : Set X)
    (hDK : D ⊆ K)
    (hx : (x : X) ∈ closure (convexHull ℝ D))
    (hD : ∀ m, 1 ≤ m → ∀ d : D,
      normToWeak K ⟨d, hDK d.property⟩ ∈
        closure ((fun a => normToWeak K (eval a)) '' family m))
    (threshold : ℕ → S → ℕ)
    (hthreshold : ∀ i s, 1 ≤ threshold i s)
    (transition : ℕ → S → M → S → Prop) (initial : S)
…

Mentions: OAI.ReflexiveFixedPoints.WeakCarrier, OAI.ReflexiveFixedPoints.normToWeak

def OAI.ReflexiveFixedPoints.adaptive_parent_return line 149

Source documentation

Choose the proved finite parent return, retaining all its witnesses.

def adaptive_parent_return
    {K : Set X} [TopologicalSpace.MetrizableSpace (WeakCarrier K)]
    {M : Type v} {S : Type w}
    (eval : M → K) (family : ℕ → Set M) (x : K) (D : Set X)
    (hDK : D ⊆ K)
    (hx : (x : X) ∈ closure (convexHull ℝ D))
    (hD : ∀ m, 1 ≤ m → ∀ d : D,
      normToWeak K ⟨d, hDK d.property⟩ ∈
        closure ((fun a => normToWeak K (eval a)) '' family m))
    (threshold : ℕ → S → ℕ)
    (hthreshold : ∀ i s, 1 ≤ threshold i s)
    (transition : ℕ → S → M → S → Prop) (initial : S)
…

Mentions: OAI.ReflexiveFixedPoints.WeakCarrier, OAI.ReflexiveFixedPoints.normToWeak