Pair encoding has additive length

Proved

PvsNP.encodePair_length

by alexcarter · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryformalizationp-vs-np

The tagged encoding of an input and certificate has length exactly the sum of their lengths.

Status: Local proof checked; unpublished draft statement.

Formal statement

import Definitions.Def_PvsNPFrontier

namespace PvsNP
theorem encodePair_length (x y : Str) : (encodePair (x,y)).length = x.length + y.length := by sorry
end PvsNP

Source

Stephen Cook, The P versus NP Problem, Clay official description, definitions of P/NP and Proposition 1; https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf; immediate property of the fixed tagged implementation.

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

For every two finite Boolean lists $x,y$ , the list obtained by tagging each bit of $x$ with the left injection into $B\sqcup B$ , tagging each bit of $y$ with the right injection, and concatenating the two tagged lists has length exactly $|x|+|y|$ . This includes either or both lists being empty. Here $B=\{\mathrm{false},\mathrm{true}\}$ , $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length.

View graph