CookLevin.decider_contract_forgets_external_certificate_v3

Proved

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

If a machine decides a Boolean predicate at a fixed time bound independently of an external certificate argument, then the predicate has the same value for all certificates.

Formal statement

import Definitions.Def_CookLevin_Cost
import Theorems.Thm_CookLevin_DecidesIn_verdict_unique
open CookLevin

theorem CookLevin.decider_contract_forgets_external_certificate_v3
    (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
  intro x w₁ w₂ y
  exact DecidesIn_verdict_unique (hdec x w₁ y) (hdec x w₂ y)

View graph