§6, p. 470 — at most (b + 2)^q legal hidden sequences

Proved

ObliviousRAM.LowerBound.card_hidden_le

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

access-patterncountingoblivious-ramp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Fix a hand capacity $b$ and a visible sequence $V$ of $q$ accessed cells. Let $H$ range over hidden choices that, paired with $V$ , form a legal action sequence from the game's initial state. Then

|\{H:(V,H)\text{ is legal}\}|\le (b+2)^q.

At each access, the hidden choice is to take, do nothing, or place one of at most $b$ held balls. This bounds the number of action histories compatible with one visible pattern.

Formalization Note Hidden sequences are functions on a finite index type, and the count filters for legal runs. Hidden m includes a placement constructor for every ball, but legality restricts it to the balls currently held.

Preamble

import Mathlib
import Definitions.Def_ObliviousRAM_LowerBound_Game

Formal statement

namespace ObliviousRAM.LowerBound
open Classical

theorem card_hidden_le {b m : ℕ} (V : List (Fin m)) :
    (Finset.univ.filter fun H : Fin V.length → Hidden m =>
      Legal b (List.ofFn fun i => (V.get i, H i))).card ≤ (b + 2) ^ V.length := 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, hidden-action observation; 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