CandidateLedger.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

All candidates and the retained ordered level

The candidate ledger keeps discarded labels. An order embedding selects the actual children. Their coefficients extend by zero to discarded candidates; restricting these coefficients to the earlier candidate prefix gives the actual prediction parameter and the exact ideal child-average identity.

structure OAI.ReflexiveFixedPoints.CandidateLedger line 23
Source documentation
A completed candidate level, including every discarded candidate.
```
structure CandidateLedger (T : OrderedTree) (k : ℕ) (Y : Type*) where
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree
def OAI.ReflexiveFixedPoints.CandidateLedger.retainedPoint line 36
def OAI.ReflexiveFixedPoints.CandidateLedger.coefficient line 39
Source documentation
Retained weights at retained candidates, and zero at discarded candidates.
```
def coefficient (W : WeightedTree T) : Fin L.count → ℝ :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeightedTree
theorem OAI.ReflexiveFixedPoints.CandidateLedger.coefficient_retain line 42
theorem OAI.ReflexiveFixedPoints.CandidateLedger.coefficient_discarded line 46
theorem OAI.ReflexiveFixedPoints.CandidateLedger.coefficient_nonneg line 50
theorem OAI.ReflexiveFixedPoints.CandidateLedger.coefficient_pos_iff line 58
theorem OAI.ReflexiveFixedPoints.CandidateLedger.coefficient_eq_zero_iff line 69
theorem OAI.ReflexiveFixedPoints.CandidateLedger.coefficientSum_eq_one line 79
Source documentation
Every full candidate parent group has exactly the actual child mass one.
```
theorem coefficientSum_eq_one (W : WeightedTree T) (p : T.Node k) :
    Prediction.coefficientSum L.parent (L.coefficient W) p = 1 := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeightedTree, OAI.ReflexiveFixedPoints.Prediction.coefficientSum
theorem OAI.ReflexiveFixedPoints.CandidateLedger.coefficient_mem_coefficientSet line 94
abbrev OAI.ReflexiveFixedPoints.CandidateLedger.Earlier line 101
Source documentation
Earlier candidates include discarded entries and omit the current entry.
```
abbrev Earlier (v : T.Node (k + 1)) := Fin (L.retain v).val
```
def OAI.ReflexiveFixedPoints.CandidateLedger.earlierInclusion line 103
def OAI.ReflexiveFixedPoints.CandidateLedger.earlierParent line 106
def OAI.ReflexiveFixedPoints.CandidateLedger.earlierPoint line 109
def OAI.ReflexiveFixedPoints.CandidateLedger.actualTheta line 112
theorem OAI.ReflexiveFixedPoints.CandidateLedger.actualTheta_mem line 116
Source documentation
The restricted candidate parameter obeys every parent budget.
```
theorem actualTheta_mem (W : WeightedTree T) (v : T.Node (k + 1)) :
    L.actualTheta W v ∈ Prediction.coefficientSet (L.earlierParent v) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeightedTree, OAI.ReflexiveFixedPoints.Prediction.coefficientSet
theorem OAI.ReflexiveFixedPoints.CandidateLedger.retained_before_iff line 136
Source documentation
The ledger's chronological order restricts to the retained level order.
```
theorem retained_before_iff (v w : T.Node (k + 1)) :
    (L.retain w).val < (L.retain v).val ↔ w < v := by
…
```

theorem OAI.ReflexiveFixedPoints.CandidateLedger.actualTheta_correction line 147

Source documentation

The correction predicted from all earlier candidates equals the correction from exactly the earlier retained children. Discarded terms vanish by definition.

theorem actualTheta_correction (W : WeightedTree T) (v : T.Node (k + 1))
    (val : Y → X) (b : X) (p : T.Node k) :
    (∑ c : L.Earlier v,
      Prediction.groupedCoefficient (L.earlierParent v) (L.actualTheta W v) p c •
        (val (L.earlierPoint v c) - b)) =
      ∑ w ∈ Finset.univ.filter (fun w => T.parent k w = p),
        if w < v then W.weight k w • (val (L.retainedPoint w) - b) else 0 := by
…

Mentions: OAI.ReflexiveFixedPoints.WeightedTree, OAI.ReflexiveFixedPoints.Prediction.groupedCoefficient

theorem OAI.ReflexiveFixedPoints.CandidateLedger.ideal_child_average_eq_residualPoint line 175

Source documentation

The actual ideal weighted child average is exactly the earlier-candidate residual point, before any nonlinear parent map is applied.

theorem ideal_child_average_eq_residualPoint (W : WeightedTree T)
    (v : T.Node (k + 1)) (val : Y → X) (b : X) (p : T.Node k) :
    (∑ w ∈ Finset.univ.filter (fun w => T.parent k w = p),
      W.weight k w • (if w < v then val (L.retainedPoint w) else b)) =
      Prediction.residualPoint (L.earlierParent v)
        (fun c => val (L.earlierPoint v c)) b (L.actualTheta W v) p := by
…

Mentions: OAI.ReflexiveFixedPoints.WeightedTree, OAI.ReflexiveFixedPoints.Prediction.residualPoint