LedgerPredictionLimits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual ideal-cutoff limits for a completed candidate ledger

The coefficient parameter is filled in only after the positive child weights exist. The exact cutoff identity proves that its prediction limit is a limit of the actual nonlinear ideal cutoff outputs.

def OAI.ReflexiveFixedPoints.CandidateLedger.predictionLimit line 28
Source documentation
The actual retained parameter inserted into the completed prediction family.
```
def predictionLimit (hK : WeaklyCompact K) (b : ℕ → K) (U : Ultrafilter ℕ)
    (v : T.Node (k + 1)) : K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact

theorem OAI.ReflexiveFixedPoints.CandidateLedger.tendsto_predictionLimit line 34

Source documentation

The limit comes from already evaluated nonlinear cutoff outputs.

theorem tendsto_predictionLimit (hK : WeaklyCompact K)
    (b : ℕ → K) (U : Ultrafilter ℕ) (v : T.Node (k + 1)) :
    Tendsto (fun j => toWeakSpace ℝ X (E.evaluate (k + 1) (L.idealOutput v (b j)) : X))
      (U : Filter ℕ) (𝓝 (toWeakSpace ℝ X (L.predictionLimit E hK b U v : X))) := by
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact

theorem OAI.ReflexiveFixedPoints.CandidateLedger.idealOutput_eq_idealCutoff line 44
Source documentation
Once the actual retained labels are identified, the ledger cutoff is exactly the switching construction's ideal cutoff.
```
theorem idealOutput_eq_idealCutoff (x : K)
    (hlabels : ∀ w, L.retainedPoint w = E.map (k + 1) w x)
    (v : T.Node (k + 1)) (b : K) :
    L.idealOutput v b = E.idealCutoff (k + 1) x b v := by
…
```

theorem OAI.ReflexiveFixedPoints.CandidateLedger.tendsto_predictionLimit_idealCutoff line 53

Source documentation

The prediction is an actual weak limit of the ideal cutoff in the final evaluated tree, with its original maps and weights.

theorem tendsto_predictionLimit_idealCutoff (hK : WeaklyCompact K)
    (b : ℕ → K) (U : Ultrafilter ℕ) (x : K)
    (hlabels : ∀ w, L.retainedPoint w = E.map (k + 1) w x)
    (v : T.Node (k + 1)) :
    Tendsto (fun j => toWeakSpace ℝ X
      (E.evaluate (k + 1) (E.idealCutoff (k + 1) x (b j) v) : X))
      (U : Filter ℕ) (𝓝 (toWeakSpace ℝ X (L.predictionLimit E hK b U v : X))) := by
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact