AnchorNonbulkBudget.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Nonbulk normalization at the manuscript's exponential bulk scale

theorem OAI.Ostmann.eventual_anchor_nonbulk_cost line 12
theorem OAI.Ostmann.eventual_scheduled_anchor_nonbulk_cost line 39

theorem OAI.Ostmann.eventual_active_anchor_nonbulk_cost line 76

Source documentation

The actual H block only pays for original active nonword slots. Negative word copies and the filler never enter this count.

theorem eventual_active_anchor_nonbulk_cost (n B : ℕ) (c ε z : ℝ)
    (hc : 0 ≤ c) (hε : 0 < ε) (hz : 0 < z)
    (hbudget : 4 * c * B ≤ ε * z) :
    ∀ᶠ L : ℝ in atTop, ∀ {I : Type*} [Fintype I]
      (role : I → CopyScheduleRole) (m : ℕ),
      z * L / 2 ≤ (m : ℝ) →
      Fintype.card {i : I // role i ≠ .word ∧ role i ≠ .outside} ≤ B →
      ∀ mass : CopyScheduleH role n → ℝ,
      (∀ h : ScheduledNonbulkH role n, Real.exp (-c * L) ≤ mass h.val) →
      (Fintype.card (ScheduledNonbulkH role n)).factorial *
        (∏ h : ScheduledNonbulkH role n, (mass h.val)⁻¹) ≤
          Real.exp (ε * (2 ^ n : ℕ) * (m : ℝ)) := by
…

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

theorem OAI.Ostmann.eventual_anchor_role_budget line 125
Source documentation
The required normalization budget is available at every sufficiently large depth, from the actual cell-role bound of Section 4.
```
theorem eventual_anchor_role_budget (R c ε : ℝ) (hc : 0 < c) (hε : 0 < ε) :
    ∀ᶠ k : ℕ in atTop, ∀ B : ℕ, (B : ℝ) ≤ cellRoleCountBound R k →
      4 * c * B ≤ ε * cellRoleScale k := by
…
```
Mentions: OAI.Ostmann.cellRoleCountBound, OAI.Ostmann.cellRoleScale