p. A:41 — for large $n$ , every machine in $S_n$ is functionally equivalent to $M$

Proved

ObfImpossibility.RiceSimulator.survivors_eventually_equivalent

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

computabilityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1rice-theorem

Let $M$ be a machine and, for $n\in\mathbb N$ , let $S_n$ be the set of machines $N$ of size $|N|=|M|$ that are $n$ -compatible with $M$ . Then there is a number $n''$ such that

\forall n>n''\ \ \forall N\in S_n:\quad [N]\equiv[M].

Only finitely many machines have size $|M|$ , and each one inequivalent to $M$ eventually leaves $S_n$ for good; the statement collects this into a single threshold. It is the step of the proof of Theorem A.2 that lets the simulator's answer stabilise on machines that $T$ must treat like $M$ .

Preamble

import Mathlib
import Definitions.Def_ObfImpossibility_RiceSimulator_Setting

Formal statement

namespace ObfImpossibility.RiceSimulator

/-- p. A:41 (proof of Theorem A.2): there is `n''` such that every machine `N ∈ S_n` with
`n > n''` satisfies `[N] ≡ [M]`. -/
theorem survivors_eventually_equivalent (M : Machine) :
    ∃ n'' : ℕ, ∀ n : ℕ, n'' < n → ∀ N ∈ survivors n M, fn N = fn M := by sorry

end ObfImpossibility.RiceSimulator

Source

Barak et al., On the (Im)possibility of Obfuscating Programs, J. ACM 59(2) (2012), author's copy, p. A:41, proof of Theorem A.2 (paragraph "We claim that S always halts")

Human review

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

View graph

p. A:41 — for large nnn, every machine in SnS_nSn​ is functionally equivalent to MMM

p. A:41 — for large $n$ , every machine in $S_n$ is functionally equivalent to $M$