pairEncode
For words w and c over an alphabet Γ, pairEncode w c is the word over Γ ⊕ Unit obtained by writing w, then the single separator symbol Sum.inr (), then c, each of the three parts written with Sum.inl.
Statement
def pairEncode {Γ : Type} (w c : List Γ) : List (Γ ⊕ Unit)
- Source
- Standard pairing of a word with a certificate, as used to state the verifier characterisation of NP (Arora & Barak, Def. 2.2; Sipser, Def. 7.16). Mathlib's Computability.Encoding provides Encoding.pair but no injective list pairing with a separator.
- Verified
- 10 Sep 2026
- Axioms
- none listed
- Used by 2
- NondeterministicPolyTimeBoundedA language L over Γ is in NP in verifier form if there are a polynomial p and a language V of words over Γ ⊕ Unit such that V is decidable…
- pair_encode_injectiveThe pair encoding is injective: if pairEncode w₁ c₁ = pairEncode w₂ c₂ then w₁ = w₂ and c₁ = c₂.
Read back from the Lean
For any type Γ, and any two lists w and c of elements of Γ, the definition pairEncode w c is the list over the type Γ ⊕ Unit (i.e., elements that are either Sum.inl g for some g : Γ, or Sum.inr ()) formed as follows, in this order: (1) each element of w, in its original order, tagged with Sum.inl; (2) a single element Sum.inr () (the unique element of the Unit summand, carrying no data); (3) each element of c, in its original order, tagged with Sum.inl. In symbols, pairEncode w c = (List.map Sum.inl w) ++ [Sum.inr ()] ++ (List.map Sum.inl c). The only arguments are Γ (an implicit type parameter), w, and c; there are no typeclass assumptions (no Fintype, DecidableEq, etc.). This is a definition, not a theorem: it introduces a function and asserts no proposition about it.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- Encodes a pair of words (w, c) as a single word over Γ ⊕ Unit, separated by Sum.inr (). -/ def pairEncode {Γ : Type} (w c : List Γ) : List (Γ ⊕ Unit) := List.map Sum.inl w ++ [Sum.inr ()] ++ List.map Sum.inl c