CharacterBulkSeparation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The true bulk is disjoint from the complementary H cells

theorem OAI.Ostmann.selectedBulkLabel_disjoint_of_original line 11

theorem OAI.Ostmann.character_bulk_label_disjoint line 41

Source documentation

The original top label is the only word slot outside the true bulk. No separation between different anchor slots is assumed or needed.

theorem character_bulk_label_disjoint {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f n : ℕ)
    (Q : Fin (m + 1) → Finset ℕ) (U : Finset ℕ)
    (R : (v : CharacterCell k) → Fin (characterCellSize r f v) → Finset ℕ)
    (hQ : ∀ i : Fin m, Q i.succ = U) (htop : Disjoint U (Q 0))
    (hR : ∀ v i, Disjoint U (R v i)) :
    ∀ a b : CopyScheduleH (fun i : Σ v, Fin (characterSize m r f v) => characterRole k i.1) n,
      selectedBulkLabel _ n m (characterBulk m r f) (characterBulk_role m r f) a ≠
        selectedBulkLabel _ n m (characterBulk m r f) (characterBulk_role m r f) b →
      Disjoint (characterFullPrimeCells m r f Q R (copyScheduleOrigin n a.val))
        (characterFullPrimeCells m r f Q R (copyScheduleOrigin n b.val)) := by
…

Mentions: OAI.Ostmann.CharacterCell, OAI.Ostmann.characterCellSize, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.characterSize, OAI.Ostmann.characterRole, OAI.Ostmann.selectedBulkLabel, OAI.Ostmann.characterBulk, OAI.Ostmann.characterBulk_role, OAI.Ostmann.characterFullPrimeCells, OAI.Ostmann.copyScheduleOrigin

theorem OAI.Ostmann.CharacterTargetWord.cell_loglog_lower line 66
theorem OAI.Ostmann.constructed_character_cells_bulk_disjoint line 73