A size that only the length decides #

A PCP verifier's coin count is a function of the input's length. The graph it reads therefore has to have a size the length alone decides, which the graph of a formula does not. The remedy is to pad every graph up to one common size — and for that one needs a size that is both computable and large enough for every input of that length.

Any FP function has one: a machine that runs in time p writes at most p |x| bits, so p bounds the output length uniformly over inputs of a given length, and Cobham.exists_exact_ruler writes p |x| marks.

Main results #

Complexity.exists_length_bound — an FP function's output is polynomially long
Complexity.exists_padRuler — hence a uniform, computable padding size

source

theorem Complexity.exists_length_bound {f : List Bool → List Bool} (hf : f ∈ FP) :

∃ (p : Polynomial ℕ), ∀ (x : List Bool), (f x).length ≤ Polynomial.eval x.length p

An FP function's output is polynomially long.

source

theorem Complexity.length_le_length_encode (φ : SAT.CNF) :

List.length φ ≤ φ.encode.length

A formula is no longer than its encoding.

source

theorem Complexity.exists_padRuler {f : List Bool → List Bool} (hf : f ∈ FP) (c : ℕ) :

∃ (padU : List Bool → List Bool) (q : Polynomial ℕ), padU ∈ FP ∧ (∀ (x : List Bool), padU x = List.replicate (padU x).length true) ∧ (∀ (x : List Bool), (padU x).length = Polynomial.eval x.length q) ∧ ∀ (x : List Bool), c * (f x).length ≤ (padU x).length

A uniform padding size: marks, as many as any input of that length can force, and as many for one input as for any other of the same length.

Rulers, structurally #

Writing a polynomial out and evaluating it is unworkable here: the constants involved are the alphabet's constraint count and the round's growth factor, and no tactic may be allowed near them. So the width is built from closure properties instead — a sum of rulers is an append, a product is a length multiplication — and no arithmetic is ever performed on a constant.

source

def Complexity.HasRuler (f : ℕ → ℕ) :

Prop

A function of the input's length that an FP string is long enough for.

Equations