SAT: Encoding Layer

This file pins down how CNFs and literals are written as List Bool, which is the bit-string format that the TM verifier will actually parse.

Format summary

  data bit b              ↦  [b, b]           (doubled)
  literal separator  "|"  ↦  [false, true]   (one undoubled pair)
  clause separator   "#"  ↦  [true, false]   (one undoubled pair)

• A variable index v : ℕ is encoded in unary as replicate v true — that is, v consecutive 1-bits. Unary.encode 0 = []. Unary is chosen (over binary) so that |encode v| ≥ v, which makes maxVar φ ≤ |φ.encode| automatic. This is what powers the PolyBalanced step in the NP-membership proof.
• A literal (sign, var) is encoded as [sign] ++ Unary.encode var — call this the raw literal encoding (a list of single bits).
• A clause is a list of raw-encoded literals, each doubled bit-by-bit, separated (and terminated) by |. An empty clause is the empty list.
• A CNF is a list of encoded clauses, each terminated by #. An empty CNF is the empty list.

Inside a clause, every bit is doubled, so the only pairs that appear are 00, 11 (data), 01 (lit sep), 10 (clause sep). The four patterns cover all four two-bit combinations and are mutually exclusive, giving a well-defined token stream for any valid encoding.

Why this format

• | and # can't collide with data because all data bits are doubled.
• No length prefixes — parsing is a single pass over the input.
• Unary variables give |encodeRaw ℓ| = ℓ.var + 1, which propagates to maxVar φ ≤ |φ.encode| (key for PolyBalanced).
• Distinguishes [] (true CNF) from [[]] (one unsatisfiable clause): the former encodes to [], the latter to [true, false].

No decode function is provided. The verifier's correctness theorem is stated directly against encode; we don't need an inverse as a Lean function to prove NP membership.

def Complexity.SAT.Unary.encode (n : ℕ) : List Bool

Unary encoding of n: n consecutive true bits. encode 0 = [].

Equations

• Complexity.SAT.Unary.encode n = List.replicate n true

@[simp]

theorem Complexity.SAT.Unary.length_encode (n : ℕ) : (encode n).length = n

The unary encoding of n has length exactly n.

@[simp]

theorem Complexity.SAT.Unary.encode_zero : encode 0 = []

Zero encodes to the empty bit list.

theorem Complexity.SAT.Unary.encode_all_true (n : ℕ) (b : Bool) : b ∈ encode n → b = true

Every bit in a unary encoding is true.

def Complexity.SAT.Lit.encodeRaw (ℓ : Lit) : List Bool

Raw literal encoding: [sign] ++ unary(var). Produces a list of single (undoubled) bits; the doubling happens at the clause level.

Equations

• ℓ.encodeRaw = ℓ.sign :: Complexity.SAT.Unary.encode ℓ.var

@[simp]

theorem Complexity.SAT.Lit.encodeRaw_length (ℓ : Lit) : ℓ.encodeRaw.length = ℓ.var + 1

The raw literal encoding has length ℓ.var + 1: one sign bit plus a unary var.

theorem Complexity.SAT.Lit.var_lt_encodeRaw_length (ℓ : Lit) : ℓ.var < ℓ.encodeRaw.length

The raw encoding of a literal has ℓ.var ≤ |encodeRaw| - 1. Key for maxVar ≤ |encode|.

theorem Complexity.SAT.Lit.encodeRaw_injective : Function.Injective encodeRaw

The raw literal encoding is injective: sign and var are recoverable.

def Complexity.SAT.doubleBits (bs : List Bool) : List Bool

Double each bit: b ↦ [b, b]. The image consists only of 00 and 11 two-bit patterns, so 01 and 10 cannot appear in doubled data.

Equations

• Complexity.SAT.doubleBits bs = List.flatMap (fun (b : Bool) => [b, b]) bs

@[simp]

theorem Complexity.SAT.doubleBits_nil : doubleBits [] = []

Doubling the empty bit list yields the empty list.

@[simp]

theorem Complexity.SAT.doubleBits_cons (b : Bool) (bs : List Bool) : doubleBits (b :: bs) = b :: b :: doubleBits bs

Doubling a cons prepends the head bit twice: doubleBits (b :: bs) = b :: b :: ….

@[simp]

theorem Complexity.SAT.doubleBits_length (bs : List Bool) : (doubleBits bs).length = 2 * bs.length

Doubling exactly doubles the length: |doubleBits bs| = 2 * |bs|.

def Complexity.SAT.Clause.encode : Clause → List Bool

Encoded clause: each literal's raw bits doubled, followed by [0,1].

Equations

• Complexity.SAT.Clause.encode [] = []
• Complexity.SAT.Clause.encode (ℓ :: ℓs) = Complexity.SAT.doubleBits ℓ.encodeRaw ++ [false, true] ++ Complexity.SAT.Clause.encode ℓs

@[simp]

theorem Complexity.SAT.Clause.encode_nil : encode [] = []

The empty clause encodes to the empty bit list.

theorem Complexity.SAT.Clause.encode_cons (ℓ : Lit) (ℓs : Clause) : encode (ℓ :: ℓs) = doubleBits ℓ.encodeRaw ++ [false, true] ++ ℓs.encode

Unfolding lemma: encoding ℓ :: ℓs emits the doubled raw literal, the [false, true] literal separator, then the encoded tail.

theorem Complexity.SAT.Clause.length_encode (c : Clause) : c.encode.length = List.foldr (fun (ℓ : Lit) (acc : ℕ) => 2 * ℓ.encodeRaw.length + 2 + acc) 0 c

Length bound on the encoded clause: each literal contributes at most 2 * |encodeRaw| + 2 bits (doubling + separator).

def Complexity.SAT.CNF.encode : CNF → List Bool

Encoded CNF: each clause followed by [1,0].

Equations

• Complexity.SAT.CNF.encode [] = []
• Complexity.SAT.CNF.encode (c :: cs) = c.encode ++ [true, false] ++ Complexity.SAT.CNF.encode cs

@[simp]

theorem Complexity.SAT.CNF.encode_nil : encode [] = []

The empty CNF encodes to the empty bit list.

theorem Complexity.SAT.CNF.encode_cons (c : Clause) (cs : CNF) : encode (c :: cs) = c.encode ++ [true, false] ++ cs.encode

Unfolding lemma: encoding c :: cs emits the encoded clause, the [true, false] clause separator, then the encoded tail.

theorem Complexity.SAT.CNF.length_encode (φ : CNF) : φ.encode.length = List.foldr (fun (c : Clause) (acc : ℕ) => c.encode.length + 2 + acc) 0 φ

Length bound: each clause contributes |c.encode| + 2 bits to the CNF.

theorem Complexity.SAT.CNF.encode_append (φ ψ : CNF) : (φ ++ ψ).encode = φ.encode ++ ψ.encode

CNF.encode is a ++-homomorphism — the per-family reduction emitters compose by output concatenation.

theorem Complexity.SAT.doubleBits_replicate_true (v : ℕ) : doubleBits (List.replicate v true) = List.replicate (2 * v) true

Doubling a run of trues doubles its length.

theorem Complexity.SAT.Clause.encode_cons' (ℓ : Lit) (ℓs : Clause) : encode (ℓ :: ℓs) = [ℓ.sign, ℓ.sign] ++ List.replicate (2 * ℓ.var) true ++ [false, true] ++ ℓs.encode

The encoded form of one literal inside a clause: doubled sign, doubled unary variable index, separator — exactly the word the reduction's literal emitter appends.

theorem Complexity.SAT.Clause.maxVar_le_encode_length (c : Clause) : c.maxVar ≤ c.encode.length

Every variable in a clause has index ≤ |c.encode|. Immediate from unary.

theorem Complexity.SAT.CNF.maxVar_le_encode_length (φ : CNF) : φ.maxVar ≤ φ.encode.length

Key bound for PolyBalanced. Every variable mentioned in φ has index at most |φ.encode|. Hence any satisfying assignment α (with unused positions truncated) has length at most |φ.encode| + 1.

theorem Complexity.SAT.doubleBits_pair_eq (bs : List Bool) (k : ℕ) (h : 2 * k + 1 < (doubleBits bs).length) : (doubleBits bs)[2 * k]? = (doubleBits bs)[2 * k + 1]?

doubleBits bs contains no [false, true] or [true, false] pair at an even-index boundary. Concretely: every pair (b_{2k}, b_{2k+1}) in doubleBits bs has b_{2k} = b_{2k+1}.