CandidateLabels.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Actual global labels of the retained candidates

Within a parent, the original positive-support embedding keeps the candidate indices. Concatenation preserves the parent order. The stage's base counter then places this entire finite sequence after all preceding sequences. Consequently the labels are globally injective even though zero-weight candidates leave gaps among the labels of retained children.

def OAI.ReflexiveFixedPoints.CandidateContext.retainedCandidate line 31
Source documentation
Retained children keep their positions in the complete candidate sequence.
```
def retainedCandidate :
    Fin (C.selectedExtension A hanchor).size ↪o Fin (C.candidateCount A hanchor) :=
…
```
theorem OAI.ReflexiveFixedPoints.CandidateContext.retainedCandidate_group line 36

theorem OAI.ReflexiveFixedPoints.CandidateContext.retainedCandidate_parent line 48

Source documentation

The original candidate index has exactly the same parent as its child.

theorem retainedCandidate_parent (v : Fin (C.selectedExtension A hanchor).size) :
    OrderedGroupConcat.parent
      (fun p => (C.group A hanchor C.runTolerance_pos p).N)
      (C.retainedCandidate A hanchor v) =
      (C.selectedExtension A hanchor).parent v :=
…

Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.parent

theorem OAI.ReflexiveFixedPoints.CandidateContext.retainedCandidate_map line 57

Source documentation

The retained node uses the same actual map as the corresponding full candidate.

theorem retainedCandidate_map (v : Fin (C.selectedExtension A hanchor).size) :
    FrontierExtension.groupValue
      (fun p => (C.group A hanchor C.runTolerance_pos p).N)
      (fun p i => (C.group A hanchor C.runTolerance_pos p).selected i)
      (C.retainedCandidate A hanchor v) =
      (C.selectedExtension A hanchor).map v := by
…

Mentions: OAI.ReflexiveFixedPoints.FrontierExtension.groupValue

def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.retainedCandidate line 81
Source documentation
Transport the retained embedding to the actual next level of the infinite tree.
```
def retainedCandidate (k : ℕ) :
    (tower D A U).toOrderedTree.Node (k + 1) ↪o
      Fin ((context D A U k).candidateCount A (context_anchor D A U k)) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_anchor
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.retainedCandidate_apply line 92
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel line 99
Source documentation
The original global candidate ordinal, with no renumbering after retention.
```
def candidateLabel (v : (tower D A U).toOrderedTree.NonrootNode) : ℕ :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel_apply line 102

theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel_group line 108

Source documentation

Exact ordinal of a retained member of a particular parent group.

theorem candidateLabel_group (k : ℕ) (p : Fin (context D A U k).frontier.size)
    (j : Fin ((context D A U k).group A (context_anchor D A U k)
      (context D A U k).runTolerance_pos p).q) :
    candidateLabel D A U
      ⟨k, ((tower D A U).nextNode k).symm
        (OrderedGroupConcat.group
          (fun p => ((context D A U k).group A (context_anchor D A U k)
            (context D A U k).runTolerance_pos p).q) p j)⟩ =
      (context D A U k).base +
        OrderedGroupConcat.offset
          (fun p => ((context D A U k).group A (context_anchor D A U k)
            (context D A U k).runTolerance_pos p).N) p +
…

Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_anchor, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.OrderedGroupConcat.group, OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset

theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_base_monotone line 139
Source documentation
The concrete candidate counter never decreases between stages.
```
theorem context_base_monotone : Monotone (fun k => (context D A U k).base) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel_lt_next_base line 146
Source documentation
Every retained label lies in its actual stage's complete candidate interval.
```
theorem candidateLabel_lt_next_base (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    candidateLabel D A U ⟨k, v⟩ < (context D A U (k + 1)).base := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context_base_le_candidateLabel line 152
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel_lt_base_of_lt line 159
Source documentation
Every candidate from an earlier level precedes the current base counter.
```
theorem candidateLabel_lt_base_of_lt {i k : ℕ} (hik : i < k)
    (v : (tower D A U).toOrderedTree.Node (i + 1)) :
    candidateLabel D A U ⟨i, v⟩ < (context D A U k).base :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel_injective line 167
Source documentation
Global injectivity follows from the actual counter recurrence and the proved within-level retained embeddings.
```
theorem candidateLabel_injective : Function.Injective (candidateLabel D A U) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidateLabel