CharacterSelectedBulk.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The original m bulk primes exclude the one top prime of each word

def OAI.Ostmann.characterBulk line 11
Source documentation
The top prime is position zero; the bulk positions are its successors.
```
def characterBulk {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f : ℕ) :
    Fin m ↪ (Σ v, Fin (characterSize m r f v)) where
…
```
Mentions: OAI.Ostmann.characterSize
def OAI.Ostmann.characterTop line 19
theorem OAI.Ostmann.characterBulk_role line 22
theorem OAI.Ostmann.characterTop_role line 25
theorem OAI.Ostmann.character_word_not_bulk line 28

theorem OAI.Ostmann.character_original_nonbulk_card line 44

Source documentation

Before copying, exactly one further word slot is outside the bulk.

theorem character_original_nonbulk_card {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f : ℕ) :
    Fintype.card {i : Σ v, Fin (characterSize m r f v) //
      i ∉ Set.range (characterBulk m r f) ∧ characterRole k i.1 ≠ .outside} ≤
        1 + ((∑ j, r j) + 2 * k) := by
…

Mentions: OAI.Ostmann.characterSize, OAI.Ostmann.characterBulk, OAI.Ostmann.characterRole

theorem OAI.Ostmann.character_selected_nonbulk_card line 71