CharacterTargetCount.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual target-word certificates satisfy the uniform cell-role bound

theorem OAI.Ostmann.character_target_cell_count line 12

Source documentation

The filler is counted once and there are exactly two anchors per step.

theorem character_target_cell_count {P : Finset ℕ} {F : ℕ → ℂ}
    {c δ U : ℝ} {k : ℕ} {T : Option (Fin k) → ℝ}
    (w : ∀ j, CharacterTargetWord P F c δ U k (T j)) :
    (((∑ j : Fin k, (w (some j)).indices.length) + (w none).indices.length + 2 * k : ℕ) : ℝ) ≤
      cellRoleCountBound (256 / (δ * c) + 2) k := by
…

Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.cellRoleCountBound

theorem OAI.Ostmann.character_target_active_count line 37

Source documentation

The extra top slot in the matching complement fits the same role budget with one further absolute unit.

theorem character_target_active_count {P : Finset ℕ} {F : ℕ → ℂ}
    {c δ U : ℝ} {k : ℕ} {T : Option (Fin k) → ℝ}
    (w : ∀ j, CharacterTargetWord P F c δ U k (T j)) :
    ((1 + ((∑ j : Fin k, (w (some j)).indices.length) + 2 * k) : ℕ) : ℝ) ≤
      cellRoleCountBound (256 / (δ * c) + 3) k := by
…

Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.cellRoleCountBound

theorem OAI.Ostmann.character_target_total_with_top line 52

theorem OAI.Ostmann.eventual_character_target_role_budget line 68

Source documentation

The depth is chosen before the endpoints, targets or their words. Every resulting actual list meets the same prescribed normalization budget.

theorem eventual_character_target_role_budget (c δ C ε : ℝ)
    (hC : 0 < C) (hε : 0 < ε) :
    ∀ᶠ k : ℕ in Filter.atTop, ∀ (P : Finset ℕ) (F : ℕ → ℂ) (U : ℝ)
      (T : Option (Fin k) → ℝ) (w : ∀ j, CharacterTargetWord P F c δ U k (T j)),
      4 * C * (1 + ((∑ j : Fin k, (w (some j)).indices.length) +
        (w none).indices.length + 2 * k) : ℕ) ≤ ε * cellRoleScale k := by
…

Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.cellRoleScale