A decider contract cannot depend on an unseen certificate

Proved

CookLevin.decider_contract_forgets_external_certificate

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

cook-levininterface-auditturing-machine

Suppose one fixed deterministic machine is required to decide $P(x,w,y)$ at a time depending only on $|x|$ , while its initial configuration contains $x$ and $y$ but not $w$ . Then $P(x,w,y)$ is independent of the unseen certificate $w$ : for every $x,y,w_1,w_2$ ,

P(x,w_1,y)=P(x,w_2,y).

This theorem records a semantic audit of external-certificate decider interfaces.

Formal statement

import Definitions.Def_CookLevin_Cost
import Theorems.Thm_CookLevin_DecidesIn_verdict_unique
open CookLevin

theorem CookLevin.decider_contract_forgets_external_certificate
    (P : List Bool → List Bool → List Bool → Bool)
    (T : Nat → Nat) (M : Machine) (k : Nat)
    (hdec : ∀ x w y : List Bool,
      DecidesIn M k (boolsToSymbols x) (boolsToSymbols y)
        (T x.length) (P x w y)) :
    ∀ x w₁ w₂ y, P x w₁ y = P x w₂ y := by sorry

Source

Semantic consequence of the exact hypothesis in https://prove2.me/theorems/48716741-a120-417c-84e7-c6ce080b0f98

View graph