CharacterDepthParameters.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform depth choices for the actual character endpoint construction

theorem OAI.Ostmann.character_strong_gap_choice line 10

Source documentation

The same fixed gap also pays the explicit nonanchor comparison margin.

theorem character_strong_gap_choice (a Ctotal Aend Bword Cdy ε : ℝ) :
    ∃ B : ℝ, 1 ≤ B ∧ 2 * (Aend + 2 * Bword + 3) + 5 ≤ B ∧
      2 * ((2 * Real.log (3 / a) + 3 + 2 * Ctotal) +
        (Aend + 2 * Bword + 1) + 2) ≤ B ∧
      2 * (Aend + 2 * Bword + 3) +
        (Cdy / a + max (Real.log 3) 0 + ε) + Real.log 2 + 6 ≤ B + 20 * Real.log a := by
…

theorem OAI.Ostmann.character_complete_depth_cutoff line 23

Source documentation

This cutoff includes the progression-input constant and strict z > 1; all bounds hold for every later depth, before the rich block chooses one.

theorem character_complete_depth_cutoff (c δ Cmass Cfinal B B₁ C₀ : ℝ)
    (hc : 0 < c) (hδ : 0 < δ) (hCmass : 0 ≤ Cmass) (hC₀ : 0 < C₀) (Kmin : ℕ) :
    ∃ K : ℕ, Kmin ≤ K ∧ 20000 ≤ K ∧ ∀ k : ℕ, K ≤ k →
      1 < cellRoleScale k ∧ C₀ ≤ Real.exp ((k : ℝ) / 10000) ∧
      Cfinal + (B + 20 * Real.log (cellRoleScale k) + 1) + 2 * B₁ + 1 ≤
        ((k - 1 : ℕ) : ℝ) * Real.log 2 - 1 ∧
      4 * Cmass *
        (characterTargetLabelBound c δ k + (k + 1) + (k + 1) : ℕ) ≤ cellRoleScale k := by
…

Mentions: OAI.Ostmann.cellRoleScale, OAI.Ostmann.characterTargetLabelBound