CharacterParameterChoice.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Choose the character gap before the depth and the growing word length

theorem OAI.Ostmann.character_gap_choice line 11

Source documentation

The initial repeat loss and density-rescaled anchor energy require one fixed gap constant. It does not depend on the later depth or selected cells.

theorem character_gap_choice (a Ctotal Aend Bword Cdy ε : ℝ) :
    ∃ B : ℝ, 1 ≤ 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_depth_and_mass_budget line 29

Source documentation

The same depth threshold pays for every label, pivot normalizer and nonbulk cost, while leaving the final permutation-entropy margin.

theorem character_depth_and_mass_budget (c δ Cmass Cfinal B B₁ : ℝ)
    (hc : 0 < c) (hδ : 0 < δ) (_hCmass : 0 ≤ Cmass) (Kmin : ℕ) :
    ∃ K : ℕ, Kmin ≤ K ∧ ∀ k : ℕ, K ≤ k →
      1 ≤ k ∧ 1 ≤ cellRoleScale k ∧
      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