§6, p. 470 — corrected counting inequality for every visible run

Proved

ObliviousRAM.LowerBound.counting_inequality

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-boundcountingoblivious-ramp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $P$ be a correct oblivious randomized player for $t$ rounds, $m$ balls, and hand capacity $b$ . For any request sequence and any positive-probability run $a$ of length $q$ ,

m^t\le (b+2)^q\operatorname{multichoose}(q,t)b^t.

The left side counts all request sequences; the right side bounds those served by the hidden histories compatible with the run's visible pattern. This is the counting statement used to obtain the logarithmic lower bound.

Formalization Note The printed proof instead gives $b^q(b+2)^q>m^t$ and infers $q>t\log_{b(b+2)}m$ . Both fail for $m=b=q=2$ , $t=7$ , when a two-access oblivious run serves all $128$ requests but the printed product is $64$ . The displayed weak inequality uses the corrected fixed-run count and keeps the paper's non-strict round-end convention.

Preamble

import Mathlib
import Definitions.Def_ObliviousRAM_LowerBound_Game

Formal statement

namespace ObliviousRAM.LowerBound

theorem counting_inequality {b m t : ℕ} (P : ObliviousPlayer b m t)
    (r : Fin t → Fin m) (a : List (Action m)) (ha : a ∈ (P.play r).support) :
    m ^ t ≤ (b + 2) ^ a.length * (Nat.multichoose a.length t * b ^ t) := by sorry

end ObliviousRAM.LowerBound

Source

Goldreich and Ostrovsky, Software protection and simulation on oblivious RAMs, J. ACM 43 (1996), p. 470, §6, proof of THEOREM 6.1, final display (corrected); https://doi.org/10.1145/233551.233553

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph