NPHard

Read back from the Lean

Fixing a type Γ (an alphabet) and a language L : Language Γ (i.e. a set of lists over Γ), the declaration defines NPHard L to mean: For **every** type Γ' (any alphabet, no finiteness or nonemptiness restriction) and **every** language L' : Language Γ', if L' is NondeterministicPolyTimeBounded Γ' L', then L' is KarpReducible Γ' Γ L' L. Spelled out, this is the standard "NP-hard" property: L is NP-hard iff every language L' over any alphabet that lies in NP is Karp-reducible to L. The reduction goes **from L' to L** (not the other way), with a poly-time computable f : List Γ' → List Γ satisfying w ∈ L' ↔ f w ∈ L. Note the two hypotheses/pieces of data are themselves definitions: - NondeterministicPolyTimeBounded Γ' L' requires a polynomial p : Polynomial ℕ and a "verifier" language V : Language (Γ' ⊕ Unit) that is decided by a deterministic TM2 machine in time at most p.eval n on inputs of length n, together with ∀ w : List Γ', w ∈ L' ↔ ∃ c : List Γ', c.length ≤ p.eval (w.length) ∧ pairEncode w c ∈ V — i.e. w ∈ L' iff there is a certificate c of length bounded by p at w.length whose encoding (w, c) lies in V. - KarpReducible Γ' Γ L' L requires a function f : List Γ' → List Γ that is poly-time computable (Nonempty (Turing.TM2ComputableInPolyTime (id) (id) f)) and satisfies ∀ w : List Γ', w ∈ L' ↔ f w ∈ L.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.