Proof of Thm A.4, p. A:42 — $\langle Z\rangle(1^t,x)=\bot$ for $t<|x|$ , $0$ otherwise, and $Z\in\Pi_N$

Proved

ObfImpossibility.RiceNoSize.Z_profile

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

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

Let $Z$ be the machine that reads its input and then returns $0$ . For all $t,x\in\mathbb N$ (inputs are unary, so $|x|=x$ ),

\langle Z\rangle(1^t,x)=\begin{cases}\bot & t<|x|,\\ 0 & \text{otherwise,}\end{cases}

and $Z\in\Pi_N$ .

The time profile of $Z$ is what the proof of Theorem A.4 must imitate: a machine that agrees with this profile on all small queries cannot be told apart from $Z$ by a simulator with a halting run.

Formalization Note In the mission's model $Z$ needs exactly $|x|$ steps (moves right over the input, halting on the first blank), so the display holds with no additive constant.

Preamble

import Mathlib
import Definitions.Def_ObfImpossibility_RiceNoSize_ProofObjects

Formal statement

namespace ObfImpossibility.RiceNoSize

/-- p. A:42: `⟨Z⟩(1^t, x) = ⊥` for `t < |x|` and `0` otherwise (with `|x| = x`), and `Z ∈ Π_N`. -/
theorem Z_profile :
    (∀ t x : ℕ, bounded Z t x = if t < x then none else some 0) ∧ Z ∈ PiN := 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 Z and the display of ⟨Z⟩(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

Proof of Thm A.4, p. A:42 — ⟨Z⟩(1t,x)=⊥\langle Z\rangle(1^t,x)=\bot⟨Z⟩(1t,x)=⊥ for t<∣x∣t<|x|t<∣x∣, 000 otherwise, and Z∈ΠNZ\in\Pi_NZ∈ΠN​

Proof of Thm A.4, p. A:42 — $\langle Z\rangle(1^t,x)=\bot$ for $t<|x|$ , $0$ otherwise, and $Z\in\Pi_N$