Prove2Me

Proof of Thm A.4, p. A:42 — a machine Nn,rN_{n,r} computing Nn,rN_{n,r} and running like ZZ on ∣x∣≤n|x|\le n

Proved
ObfImpossibility.RiceNoSize.exists_N

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

computabilityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1turing-machines

For all n,r∈Nn,r\in\mathbb N there is a machine NN that computes the function

Nn,r(x)={0∣x∣≤n,1∣x∣=n+1,r∣x∣≥n+2,N_{n,r}(x)=\begin{cases}0 & |x|\le n,\\ 1 & |x|=n+1,\\ r & |x|\ge n+2,\end{cases}

and runs in time ∣x∣|x| with output 00 on inputs with ∣x∣≤n|x|\le n, exactly as ZZ does: for all xx with ∣x∣≤n|x|\le n and all tt,

⟨N⟩(1t,x)=⟨Z⟩(1t,x).\langle N\rangle(1^t,x)=\langle Z\rangle(1^t,x).

In particular ⟨Z⟩(1t,x)=⟨N⟩(1t,x)\langle Z\rangle(1^t,x)=\langle N\rangle(1^t,x) for all t,∣x∣≤nt,|x|\le n.

Together with the previous milestone this gives S⟨N⟩()=S⟨Z⟩()=0S^{\langle N\rangle}()=S^{\langle Z\rangle}()=0 once nn bounds the queries of S⟨Z⟩()S^{\langle Z\rangle}().

Formalization Note Inputs are unary (∣x∣=x|x|=x) and the output rr is a natural number.

Preamble
import Mathlib
import Definitions.Def_ObfImpossibility_RiceNoSize_ProofObjects
Formal statement
namespace ObfImpossibility.RiceNoSize

/-- p. A:42: for all `n` and `r` there is a machine `N_{n,r}` computing the function
`N_{n,r}` that runs like `Z` (in time `|x|`, output `0`) on every input `x` with `|x| ≤ n`;
in particular `⟨Z⟩(1^t, x) = ⟨N_{n,r}⟩(1^t, x)` for all `t` and all `|x| ≤ n`. -/
theorem exists_N (n r : ℕ) :
    ∃ N : Machine, fn N = Nfun n r ∧
      ∀ x : ℕ, x ≤ n → ∀ t : ℕ, bounded N t x = bounded Z t x := by sorry

end ObfImpossibility.RiceNoSize
Source
Barak et al., On the (Im)possibility of Obfuscating Programs, J. ACM 59(2) (2012), author's copy, p. A:42, proof of Theorem A.4 (the machine N_{n,r} and "For any t, |x| ≤ n, ⟨Z⟩(1^t, x) = ⟨N_{n,r}⟩(1^t, x).")
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