CellRoleBudget.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Absorption of the cell-role count

Section 4 fixes ε = 1/10000, bounds the number of selected cell roles by C (k+1) exp(2 ε k), and uses the scale z = exp(3 ε k). Their ratio tends to zero, so every fixed positive proportion of z eventually absorbs the role count. This is an elementary numerical step, with no published input.

def OAI.Ostmann.cellRoleEpsilon line 20
Source documentation
The fixed small parameter used in the character selection.
```
noncomputable def cellRoleEpsilon : ℝ := 1 / 10000
```
def OAI.Ostmann.cellRoleCountBound line 23
Source documentation
Upper bound for all selected cell roles, including the anchors.
```
noncomputable def cellRoleCountBound (C : ℝ) (k : ℕ) : ℝ :=
…
```
def OAI.Ostmann.cellRoleScale line 27
Source documentation
The larger exponential scale which absorbs the cell-role count.
```
noncomputable def cellRoleScale (k : ℕ) : ℝ :=
…
```
theorem OAI.Ostmann.cellRoleScale_pos line 30
theorem OAI.Ostmann.cellRoleCountBound_nonneg line 32
theorem OAI.Ostmann.cellRoleCountBound_div_scale line 37
theorem OAI.Ostmann.tendsto_cellRoleCountBound_div_scale line 46
Source documentation
The manuscript's n_max / z → 0, with its fixed value of epsilon.
```
theorem tendsto_cellRoleCountBound_div_scale (C : ℝ) :
    Tendsto (fun k : ℕ => cellRoleCountBound C k / cellRoleScale k)
      atTop (𝓝 0) := by
…
```
Mentions: OAI.Ostmann.cellRoleCountBound, OAI.Ostmann.cellRoleScale
theorem OAI.Ostmann.eventually_cellRoleCountBound_le line 60
Source documentation
Any prescribed positive budget eventually absorbs the entire role count.
```
theorem eventually_cellRoleCountBound_le (C b : ℝ) (hb : 0 < b) :
    ∀ᶠ k : ℕ in atTop, cellRoleCountBound C k ≤ b * cellRoleScale k := by
…
```
Mentions: OAI.Ostmann.cellRoleCountBound, OAI.Ostmann.cellRoleScale
theorem OAI.Ostmann.exists_cellRoleCount_cutoff line 68
Source documentation
A single cutoff works for every actual list whose number of roles obeys the manuscript's upper bound.
```
theorem exists_cellRoleCount_cutoff (C b : ℝ) (hb : 0 < b) :
    ∃ K : ℕ, ∀ k : ℕ, K ≤ k → ∀ n : ℕ,
      (n : ℝ) ≤ cellRoleCountBound C k → (n : ℝ) ≤ b * cellRoleScale k := by
…
```
Mentions: OAI.Ostmann.cellRoleCountBound, OAI.Ostmann.cellRoleScale