OAI/NumberTheory/Ostmann/Construction/FinalEnergyCutoff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed epsilon leaves room for the actual final energy cost

  1. theorem OAI.Ostmann.eventual_final_energy_margin line 14

    Source documentation

    With the manuscript's gap B + 20 log z, even the direct finite-history energy estimate is absorbed by the final factorial gain. All other costs are fixed before the depth is selected.

    theorem eventual_final_energy_margin (B F₀ H D B₁ : ℝ) :
    ∀ᶠ k : ℕ in atTop,
      (4 * ((B + 20 * Real.log (cellRoleScale k)) + F₀) -
        (B + 20 * Real.log (cellRoleScale k)) + H) + D + 2 * B₁ + 1 ≤
          (k : ℝ) * Real.log 2 - 1 := by
…

    Mentions: OAI.Ostmann.cellRoleScale