Fact (3), p. A:41 — if $[M]\not\equiv[N]$ then $N$ is eventually not $n$ -compatible with $M$

Proved

ObfImpossibility.RiceSimulator.fact_3_eventually_incompatible

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

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

Let $M$ and $N$ be machines whose computed partial functions differ, $[M]\not\equiv[N]$ . Then there is a number $n'$ such that

\forall n>n':\quad N \text{ is not } n\text{-compatible with } M.

Functional inequivalence is witnessed by a finite amount of bounded computation, and compatibility at stage $n$ inspects all budgets and inputs up to $n$ ; this fact is what eventually removes every inequivalent machine from the simulator's candidate sets $S_n$ in the proof of Theorem A.2.

Formalization Note $[M]\not\equiv[N]$ is inequality of the partial functions Code.eval M and Code.eval N: they may differ in a value or in where they are defined.

Preamble

import Mathlib
import Definitions.Def_ObfImpossibility_RiceSimulator_Setting

Formal statement

namespace ObfImpossibility.RiceSimulator

/-- Fact (3), p. A:41: if `[M] ≢ [N]` then there is `n'` such that `N` is not
`n`-compatible with `M` for all `n > n'`. -/
theorem fact_3_eventually_incompatible (M N : Machine) (h : fn M ≠ fn N) :
    ∃ n' : ℕ, ∀ n : ℕ, n' < n → ¬ Compatible n N 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, fact (3)

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

Fact (3), p. A:41 — if [M]≢[N][M]\not\equiv[N][M]≡[N] then NNN is eventually not nnn-compatible with MMM

Fact (3), p. A:41 — if $[M]\not\equiv[N]$ then $N$ is eventually not $n$ -compatible with $M$