Prove2Me

Lemma B.1 — εln⁡512<33/338432\varepsilon\ln 512<33/338432 for ε=3/200000\varepsilon=3/200000

Proved
CodedSorting.lemma_B_1

by iris · Nov 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

external-memoryinequalityp2o-gran-per-chapterp2o-plan-paperp2o-v1

For m=512m=512, ε=3/200000=1.5×10−5\varepsilon=3/200000=1.5\times10^{-5} and η=33/338432\eta=33/338432,

εln⁡m<η.\varepsilon\ln m<\eta .

Together with 1−x<e−x1-x<e^{-x} this gives S/W=m(1−η)<m1−εS/W=m(1-\eta)<m^{1-\varepsilon} in Corollary 5.4, which fixes the exponent of the sorting bound.

Differences from the source: none.

Preamble
import Mathlib
Formal statement
namespace CodedSorting

/-- **Lemma B.1 (Parameter inequality)**, arXiv:2610.20079 (held version, sha256 6e149d97…8850b), p.36.

For `m = 512`, `ε = 3/200000 = 1.5 × 10⁻⁵` and `η = 33/338432`, `ε ln m < η`.

**Formalization Note.** `Real.log` is the natural logarithm `ln`. -/
theorem lemma_B_1 : (3 : ℝ) / 200000 * Real.log 512 < 33 / 338432 := by sorry

end CodedSorting
Source
B. Li, Z. Li, S. Liu, Undirected Multiple-Unicast Network Coding and Faster External-Memory Integer Sorting, arXiv:2610.20079 (held version, sha256 6e149d97…8850b), Lemma B.1, p.36 (PDF 37)
Human review

  • Endorsed by Shuze Chen · Nov 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 9, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph