OAI/NumberTheory/Ostmann/Characters/CharacterDepthChoice.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One fixed depth meets the role-count and final entropy budgets

  1. theorem OAI.Ostmann.cellRoleEpsilon_margin line 9
  2. theorem OAI.Ostmann.log_cellRoleScale line 14
  3. theorem OAI.Ostmann.character_depth_cutoff line 20

    Source documentation

    The threshold can be chosen before the late-block density increment. Every resulting depth above it meets both budgets with the same constants.

    theorem character_depth_cutoff (C R b : ℝ) (hb : 0 < b) (Kmin : ℕ) :
    ∃ K : ℕ, Kmin ≤ K ∧ ∀ k : ℕ, K ≤ k →
      1 ≤ k ∧ 1 ≤ cellRoleScale k ∧
        C + 20 * Real.log (cellRoleScale k) ≤ (k : ℝ) * Real.log 2 - 1 ∧
        cellRoleCountBound R k ≤ b * cellRoleScale k := by
…

    Mentions: OAI.Ostmann.cellRoleScale, OAI.Ostmann.cellRoleCountBound