PredictionCutoff.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual retained coefficient parameter predicts the ideal cutoff

Earlier retained children carry their labels. The current and all later children carry one common point. Discarded candidates remain in the earlier parameter domain with zero coefficient. The identity is proved before applying the identical nonlinear maps on both sides.

def OAI.ReflexiveFixedPoints.CandidateLedger.actualParameter line 28
Source documentation
The actual coefficients are used only after the retained weights are known.
```
def actualParameter (W : WeightedTree T) (v : T.Node (k + 1)) :
    Prediction.coefficientSet (L.earlierParent v) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeightedTree, OAI.ReflexiveFixedPoints.Prediction.coefficientSet
def OAI.ReflexiveFixedPoints.CandidateLedger.idealOutput line 33
Source documentation
The ideal cutoff immediately after the current descendant block switches.
```
def idealOutput (v : T.Node (k + 1)) (b : K) (w : T.Node (k + 1)) : K :=
…
```

theorem OAI.ReflexiveFixedPoints.CandidateLedger.childAverage_idealOutput line 37

Source documentation

The actual ideal child average equals its residual candidate prediction.

theorem childAverage_idealOutput (E : TreeEvaluation W K)
    (v : T.Node (k + 1)) (b : K) (p : T.Node k) :
    E.childAverage k (L.idealOutput v b) p =
      Prediction.residualInput E k (L.earlierParent v) (L.earlierPoint v)
        b (L.actualParameter W v) p := by
…

Mentions: OAI.ReflexiveFixedPoints.TreeEvaluation, OAI.ReflexiveFixedPoints.Prediction.residualInput

theorem OAI.ReflexiveFixedPoints.CandidateLedger.evaluate_idealOutput line 56
Source documentation
The ideal cutoff's root output is the already specified prediction, with actual coefficients inserted only after all weights are fixed.
```
theorem evaluate_idealOutput (E : TreeEvaluation W K)
    (v : T.Node (k + 1)) (b : K) :
    E.evaluate (k + 1) (L.idealOutput v b) =
      Prediction.evaluatedPrediction E k (L.earlierParent v) (L.earlierPoint v)
        b (L.actualParameter W v) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeEvaluation, OAI.ReflexiveFixedPoints.Prediction.evaluatedPrediction