Rational hitting lists: polynomial-time parameters

The parameters of the hitting-list generator are computed in polynomial time from the number of variables n and the node-count bound s, both in unary. Every parameter is polynomial in n + s + 1 (Cslib.Circuits.Rational.Parameters.polynomial_M, Cslib.Circuits.Rational.Parameters.polynomial_H), so its unary encoding has polynomial length; the later stages use these parameters as loop counts, dimensions and moduli. The rank bound, the dimension allowance and the threshold rankBound s * delta n s are fixed polynomials. The exponent is a binary logarithm of the threshold. The ambient dimension 2 ^ (exponent + 1) is the power of two at the ceiling logarithm of the threshold plus one (Parameters.ambientDimension_eq), and the cyclotomic degree is half of it. The truncation, the grid size and the matrix dimension follow by unary arithmetic.

Each certificate is stated compositionally, for parameters computed in unary from an arbitrary input, and registered with fun_prop.

Main definitions

• Cslib.Circuits.Rational.threshold: the rank expansion threshold rankBound s * delta n s.
• Cslib.Circuits.Rational.generatorParameters: the parameters (truncation, exponent, ambientDimension, degree, gridSize, matrixDimension) of the generator.

Main results

• Cslib.Circuits.Rational.Parameters.ambientDimension_eq, Cslib.Circuits.Rational.Parameters.degree_eq: the ambient dimension and the cyclotomic degree in certifiable form.
• Cslib.Circuits.Rational.computableInPolyTime_exponent, Cslib.Circuits.Rational.computableInPolyTime_ambientDimension, Cslib.Circuits.Rational.computableInPolyTime_truncation, Cslib.Circuits.Rational.computableInPolyTime_gridSize, Cslib.Circuits.Rational.computableInPolyTime_matrixDimension and their companions: unary certificates for every parameter.
• Cslib.Circuits.Rational.computableInPolyTime_generatorParameters: all parameters at once, from unary (n, s).
• Cslib.Circuits.Rational.computableInPolyTime_hittingList_dimension, Cslib.Circuits.Rational.computableInPolyTime_hittingList_dimension_binary: the common dimension of the hitting list, in unary and in binary.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.Circuits.Rational.threshold (n s : ℕ) : ℕ

The rank expansion threshold: the ambient dimension is the least power of two above it.

theorem Cslib.Circuits.Rational.Parameters.ambientDimension_eq (n s : ℕ) : ambientDimension n s = 2 ^ Nat.clog 2 (threshold n s + 1)

The ambient dimension is two to the ceiling logarithm of the threshold plus one.

theorem Cslib.Circuits.Rational.Parameters.degree_eq (n s : ℕ) : CyclotomicRing.degree (exponent n s) = ambientDimension n s / 2

The cyclotomic degree is half of the ambient dimension.

theorem Cslib.Circuits.Rational.hittingList_dimension (n s : ℕ) : (hittingList n s).dimension = Generator.matrixDimension (Parameters.exponent n s)

The common dimension of the hitting list is the generator's matrix dimension.

def Cslib.Circuits.Rational.generatorParameters (n s : ℕ) : ℕ × ℕ × ℕ × ℕ × ℕ × ℕ

The parameters (N, e, M, Dg, H, d) of the hitting-list generator: the truncation, the exponent, the ambient dimension, the cyclotomic degree, the grid size and the matrix dimension.

theorem Cslib.Circuits.Rational.computableInPolyTime_w {α : Type} {input : α ↪ List Bool} {n : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Parameters.w (n a)) input Turing.MultiTapeTM.encUnary

The number of matrices in a lifted tuple, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_rankBound {α : Type} {input : α ↪ List Bool} {s : α → ℕ} (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Parameters.rankBound (s a)) input Turing.MultiTapeTM.encUnary

The rank bound, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_delta {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Parameters.delta (n a) (s a)) input Turing.MultiTapeTM.encUnary

The dimension allowance, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_threshold {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => threshold (n a) (s a)) input Turing.MultiTapeTM.encUnary

The rank expansion threshold, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_exponent {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Parameters.exponent (n a) (s a)) input Turing.MultiTapeTM.encUnary

The exponent, the binary logarithm of the threshold, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_ambientDimension {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Parameters.ambientDimension (n a) (s a)) input Turing.MultiTapeTM.encUnary

The ambient dimension, in unary, by repeated doubling up to the ceiling logarithm.

theorem Cslib.Circuits.Rational.computableInPolyTime_degree {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => CyclotomicRing.degree (Parameters.exponent (n a) (s a))) input Turing.MultiTapeTM.encUnary

The cyclotomic degree, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_truncation {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Parameters.truncation (n a) (s a)) input Turing.MultiTapeTM.encUnary

The number of retained columns, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_gridSize {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Parameters.gridSize (n a) (s a)) input Turing.MultiTapeTM.encUnary

The grid side length, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_matrixDimension {α : Type} {input : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Generator.matrixDimension (Parameters.exponent (n a) (s a))) input Turing.MultiTapeTM.encUnary

The matrix dimension of the generator, in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_generatorParameters : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => generatorParameters p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)))))

All generator parameters, in unary, from n and s in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_hittingList_dimension : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => (hittingList p.1 p.2).dimension) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary

The common dimension of the hitting list, in unary, from n and s in unary.

theorem Cslib.Circuits.Rational.computableInPolyTime_hittingList_dimension_binary : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => (hittingList p.1 p.2).dimension) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat

The common dimension of the hitting list, in binary, from n and s in unary.