ActiveNonbulkCount.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Counting only original active nonword slots

Outside slots cannot enter H. In particular the negative copy of the whole word must not be charged to the nonbulk harmonic normalization.

def OAI.Ostmann.survivorTrace line 16

Source documentation

A binary trace suffices on surviving vertices: at a fixed predecessor, copying and retaining are mutually exclusive.

def survivorTrace {I : Type*} : (n : ℕ) → CopyScheduleVertex I n → (Fin n → Bool)
  | 0, _ => Fin.elim0
  | n + 1, .inl (b, i) => Fin.snoc (survivorTrace n i) b
  | n + 1, .inr i => Fin.snoc (survivorTrace n i) false

Mentions: OAI.Ostmann.CopyScheduleVertex

theorem OAI.Ostmann.survivorTrace_origin_injective line 21
theorem OAI.Ostmann.copyScheduleRole_origin_word line 69

theorem OAI.Ostmann.scheduledNonbulkH_card_active line 82

Source documentation

The coefficient counts only original slots which can actually enter H.

theorem scheduledNonbulkH_card_active {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (n : ℕ) :
    Fintype.card (ScheduledNonbulkH role n) ≤
      2 ^ n * Fintype.card {i : I // role i ≠ .word ∧ role i ≠ .outside} := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduledNonbulkH