GlobalCandidateOrdinals.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Global candidate ordinals

Every level reserves its full candidate interval. Retained candidates are indexed by an order embedding into that interval. Hence rejected candidates still consume their original ordinal, and labels at distinct levels cannot collide. None of the arithmetic requires candidate counts to be positive.

def OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.base line 19
Source documentation
Number of candidate ordinals consumed before a given level.
```
def base (count : ℕ → ℕ) : ℕ → ℕ
  | 0 => 0
  | k + 1 => base count k + count k
```
theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.base_zero line 23
theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.base_succ line 25
theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.base_monotone line 29
Source documentation
Any counter with the candidate-count recurrence is monotone.
```
theorem base_monotone (B count : ℕ → ℕ)
    (hstep : ∀ k, B (k + 1) = B k + count k) : Monotone B := by
…
```
theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.base_mono line 36

def OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label line 42

Source documentation

The original ordinal of a retained entry.

def label (B : ℕ → ℕ) (embed : ∀ k, Fin (size k) ↪o Fin (count k))
    (s : Σ k, Fin (size k)) : ℕ := B s.1 + (embed s.1 s.2).val

theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label_mk line 45
theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.base_le_label line 49
theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label_lt_next line 55

theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label_lt_of_level_lt line 63

Source documentation

Every earlier retained candidate lies before a later level's base.

theorem label_lt_of_level_lt (B : ℕ → ℕ)
    (hstep : ∀ k, B (k + 1) = B k + count k)
    (embed : ∀ k, Fin (size k) ↪o Fin (count k)) {k j : ℕ}
    (hkj : k < j) (v : Fin (size k)) : label B embed ⟨k, v⟩ < B j :=
…

Mentions: OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label

theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label_lt_of_level_lt_label line 70

theorem OAI.ReflexiveFixedPoints.GlobalCandidateOrdinals.label_injective line 79

Source documentation

Labels distinguish both levels and retained entries within a level.

theorem label_injective (B : ℕ → ℕ)
    (hstep : ∀ k, B (k + 1) = B k + count k)
    (embed : ∀ k, Fin (size k) ↪o Fin (count k)) :
    Function.Injective
      (fun s : Σ k, Fin (size k) => B s.1 + (embed s.1 s.2).val) := by
…