CandidateDetectors.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual retained functionals and their detector estimates

The functionals come from the legal candidate records. Their original prefix budgets equal the global retained labels' budgets. The stored proper-ancestor list is the actual final tree path, so the same record also supplies the required path-displacement estimate.

theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix_nextBudget line 27
Source documentation
The budget fixed before selection is the retained node's original budget.
```
theorem candidatePrefix_nextBudget (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    (context D A U k).nextBudget (candidatePrefix D A U k v) =
      OrderedTree.retainedBudget (candidateLabel D A U) ⟨k, v⟩ := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateFunctional_norm line 35
Source documentation
The actual chosen detector has dual norm at most one.
```
theorem candidateFunctional_norm (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    ‖candidateFunctional D A U k v‖ ≤ 1 :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateFunctional
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateFunctional_detector line 42
Source documentation
The original record separates its output from every point of its actual compact prediction detector set.
```
theorem candidateFunctional_detector (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) (z : X)
    (hz : z ∈ (context D A U k).detectorSet (candidatePrefix D A U k v)) :
    1 - OrderedTree.retainedBudget (candidateLabel D A U) ⟨k, v⟩ ≤
      candidateFunctional D A U k v
        (((tower D A U).toEvaluation.map (k + 1) v A.x : X) - z) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateFunctional
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateFunctional_dense_detector line 56
Source documentation
Every prescribed dense test point at this depth lies in the detector.
```
theorem candidateFunctional_dense_detector (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) (i : ℕ) (hi : i < k + 1) :
    1 - OrderedTree.retainedBudget (candidateLabel D A U) ⟨k, v⟩ ≤
      candidateFunctional D A U k v
        (((tower D A U).toEvaluation.map (k + 1) v A.x : X) - D.z i) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateFunctional
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidate_path_displacement line 73
Source documentation
The actual record's ancestor budget controls the final tree's path sum.
```
theorem candidate_path_displacement (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    (tower D A U).toEvaluation.pathDisplacement (k + 1) v
        ((tower D A U).toEvaluation.map (k + 1) v A.x) ≤
      OrderedTree.retainedBudget (candidateLabel D A U) ⟨k, v⟩ := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.OrderedTree.retainedBudget, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel