Polynomial-time rational hitting-list generator

This module assembles the polynomial-time rational hitting-list generator from the certified parameter schedule (Complexity/Computability/Circuit/Rational/Runtime/Parameters.lean), the staged division-free integer determinant (Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean), the integer lift tables (Complexity/Computability/Circuit/Rational/Runtime/Lift.lean), the reduced-rational binary encoding (Complexity/Computability/Circuit/Rational/Runtime/Encode.lean), and the per-point Cramer normalization (Complexity/Computability/Circuit/Rational/Runtime/Point.lean).

Given parameters (n, s), gridPointWords enumerates the three-dimensional grid {1, …, H}³ in lexicographic order and collects the encoded normalized tuples emitted at all nonsingular points. outputWord prepends the self-delimiting binary encodings of the common matrix dimension M * Dg and the emitted tuple count words.length, and hittingListWord n s instantiates outputWord at Parameters.truncation n s, Parameters.ambientDimension n s, CyclotomicRing.degree (Parameters.exponent n s), and Parameters.gridSize n s, agreeing with encodeOutput (hittingList n s) for all n, s : ℕ (hittingListWord_eq).

For a standalone List Bool → List Bool generator, inputWord n s encodes (n, s) as the unary word true ^ n ++ [false] ++ true ^ s, parseInput recovers some (n, s) when 1 ≤ n, 1 ≤ s, and w = inputWord n s (and none otherwise), and hittingGenerator emits encodeOutput (hittingList n s) on valid inputs and [] on malformed inputs.

Main definitions

• Cslib.Circuits.Rational.gridPointWords: list of encoded tuples emitted across the {1, …, H}³ grid.
• Cslib.Circuits.Rational.outputWord, Cslib.Circuits.Rational.hittingListWord: complete binary encoding of the generator output for fixed parameters and for the selected parameter schedule.
• Cslib.Circuits.Rational.inputWord, Cslib.Circuits.Rational.parseInput: unary input format true ^ n ++ [false] ++ true ^ s and its parser.
• Cslib.Circuits.Rational.hittingGenerator: the standalone List Bool → List Bool hitting-list generator.

Main results

• Cslib.Circuits.Rational.gridPointWords_eq, Cslib.Circuits.Rational.outputWord_eq, Cslib.Circuits.Rational.hittingListWord_eq: agreement with ExecutableGenerator.output and encodeOutput (hittingList n s).
• Cslib.Circuits.Rational.hittingList_polytime: (n, s) ↦ encodeOutput (hittingList n s) is computable in polynomial time from unary (n, s).
• Cslib.Circuits.Rational.parseInput_eq_some_iff, Cslib.Circuits.Rational.parseInput_inputWord, Cslib.Circuits.Rational.parseInput_eq_none_iff: exact characterization of parseInput.
• Cslib.Circuits.Rational.hittingGenerator_inputWord, Cslib.Circuits.Rational.hittingGenerator_eq_nil, Cslib.Circuits.Rational.hittingGenerator_eq_nil_of_parseInput_eq_none: behavior of hittingGenerator on valid and malformed inputs.
• Cslib.Circuits.Rational.hittingGenerator_polytime: hittingGenerator is computable in polynomial time over encBits.
• Cslib.Circuits.Rational.hittingGenerator_spec: packaged end-to-end polynomial-time, dimension-bound, encoding-length, and hitting specification for hittingGenerator.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf787 (files lean/OAI/Computability/RationalHitting/GridEnumeration.lean and PolynomialTime.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

Grid enumeration and complete output encoding

def Cslib.Circuits.Rational.gridPointWords (n N M Dg H : ℕ) : List (List Bool)

List of encoded normalized tuples emitted across the {1, …, H}³ grid in lexicographic order.

def Cslib.Circuits.Rational.outputWord (n N M Dg H : ℕ) : List Bool

Complete binary encoding of the generator output for parameters (n, N, M, Dg, H): the encoded matrix dimension M * Dg, the encoded emitted tuple count, and the concatenation of all emitted tuple encodings.

def Cslib.Circuits.Rational.hittingListWord (n s : ℕ) : List Bool

Complete binary encoding of the hitting list at the selected parameters for (n, s).

theorem Cslib.Circuits.Rational.gridPointWords_eq (n N e H : ℕ) : gridPointWords n N (CyclotomicRing.dimension e) (CyclotomicRing.degree e) H = List.map encodeTuple (ExecutableGenerator.output n N e H).tuples

gridPointWords produces the list of encoded tuples of ExecutableGenerator.output.

theorem Cslib.Circuits.Rational.outputWord_eq (n N e H : ℕ) : outputWord n N (CyclotomicRing.dimension e) (CyclotomicRing.degree e) H = encodeOutput (ExecutableGenerator.output n N e H)

outputWord agrees with encodeOutput (ExecutableGenerator.output n N e H).

theorem Cslib.Circuits.Rational.hittingListWord_eq (n s : ℕ) : hittingListWord n s = encodeOutput (hittingList n s)

hittingListWord n s agrees with encodeOutput (hittingList n s) for all n, s : ℕ.

Unary input format and standalone generator

def Cslib.Circuits.Rational.inputWord (n s : ℕ) : List Bool

Unary input word true ^ n ++ [false] ++ true ^ s representing the parameter pair (n, s).

@[simp]

theorem Cslib.Circuits.Rational.length_inputWord (n s : ℕ) : (inputWord n s).length = n + s + 1

The length of inputWord n s is n + s + 1.

@[simp]

theorem Cslib.Circuits.Rational.idxOf_false_inputWord (n s : ℕ) : List.idxOf false (inputWord n s) = n

The first false bit of inputWord n s occurs at index n.

def Cslib.Circuits.Rational.parseInput (w : List Bool) : Option (ℕ × ℕ)

Parse a valid unary input word inputWord n s with 1 ≤ n and 1 ≤ s, returning none on malformed inputs.

theorem Cslib.Circuits.Rational.parseInput_eq_some_iff (w : List Bool) (n s : ℕ) : parseInput w = some (n, s) ↔ 1 ≤ n ∧ 1 ≤ s ∧ w = inputWord n s

parseInput w = some (n, s) holds if and only if 1 ≤ n, 1 ≤ s, and w = inputWord n s.

@[simp]

theorem Cslib.Circuits.Rational.parseInput_inputWord {n s : ℕ} (hn : 1 ≤ n) (hs : 1 ≤ s) : parseInput (inputWord n s) = some (n, s)

parseInput recovers (n, s) on inputWord n s whenever 1 ≤ n and 1 ≤ s.

theorem Cslib.Circuits.Rational.parseInput_eq_none_iff (w : List Bool) : parseInput w = none ↔ ¬∃ (n : ℕ) (s : ℕ), 1 ≤ n ∧ 1 ≤ s ∧ w = inputWord n s

parseInput w = none holds if and only if w is not of the form inputWord n s with 1 ≤ n and 1 ≤ s.

def Cslib.Circuits.Rational.hittingGenerator (w : List Bool) : List Bool

The standalone rational hitting-list generator on bit words: parses a unary input word inputWord n s with 1 ≤ n and 1 ≤ s and emits encodeOutput (hittingList n s), or [] on malformed inputs.

@[simp]

theorem Cslib.Circuits.Rational.hittingGenerator_inputWord {n s : ℕ} (hn : 1 ≤ n) (hs : 1 ≤ s) : hittingGenerator (inputWord n s) = encodeOutput (hittingList n s)

On a valid unary input inputWord n s with 1 ≤ n and 1 ≤ s, hittingGenerator emits encodeOutput (hittingList n s).

theorem Cslib.Circuits.Rational.hittingGenerator_eq_nil_of_parseInput_eq_none {w : List Bool} (h : parseInput w = none) : hittingGenerator w = []

On any word where parseInput w = none, hittingGenerator w = [].

theorem Cslib.Circuits.Rational.hittingGenerator_eq_nil {w : List Bool} (h : ¬∃ (n : ℕ) (s : ℕ), 1 ≤ n ∧ 1 ≤ s ∧ w = inputWord n s) : hittingGenerator w = []

On any malformed input word not of the form inputWord n s with 1 ≤ n and 1 ≤ s, hittingGenerator w = [].

Polynomial-time certificates

theorem Cslib.Circuits.Rational.computableInPolyTime_gridPointWords {α : Type} {encIn : α ↪ List Bool} {n N M Dg H : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hH : Turing.MultiTapeTM.ComputableInPolyTime H encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => gridPointWords (n x) (N x) (M x) (Dg x) (H x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Enumerating the encoded tuples across the {1, …, H}³ grid is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_outputWord {α : Type} {encIn : α ↪ List Bool} {n N M Dg H : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hH : Turing.MultiTapeTM.ComputableInPolyTime H encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => outputWord (n x) (N x) (M x) (Dg x) (H x)) encIn Turing.MultiTapeTM.encBits

Computing the complete output encoding outputWord is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_hittingListWord {α : Type} {encIn : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => hittingListWord (n x) (s x)) encIn Turing.MultiTapeTM.encBits

Computing hittingListWord from unary (n, s) is polynomial-time.

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

The encoded rational hitting list (n, s) ↦ encodeOutput (hittingList p.1 p.2) is computable in polynomial time from unary (n, s).

theorem Cslib.Circuits.Rational.computableInPolyTime_hittingList {α : Type} {encIn : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => encodeOutput (hittingList (n x) (s x))) encIn Turing.MultiTapeTM.encBits

Compositional polynomial-time certificate for encodeOutput (hittingList (n x) (s x)).

theorem Cslib.Circuits.Rational.computableInPolyTime_inputWord {α : Type} {encIn : α ↪ List Bool} {n s : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => inputWord (n x) (s x)) encIn Turing.MultiTapeTM.encBits

Constructing the unary input word inputWord is polynomial-time.

theorem Cslib.Circuits.Rational.parseInput_polytime : Turing.MultiTapeTM.ComputableInPolyTime parseInput Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary))

Parsing a unary input word with parseInput is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_parseInput {α : Type} {encIn : α ↪ List Bool} {w : α → List Bool} (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => parseInput (w x)) encIn (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary))

Compositional polynomial-time certificate for parseInput.

theorem Cslib.Circuits.Rational.hittingGenerator_polytime : Turing.MultiTapeTM.ComputableInPolyTime hittingGenerator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

The standalone rational hitting-list generator hittingGenerator is computable in polynomial time on a multi-tape Turing machine.

theorem Cslib.Circuits.Rational.hittingGenerator_spec : Turing.MultiTapeTM.ComputableInPolyTime hittingGenerator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits ∧ ∀ (n s : ℕ), 1 ≤ n → 1 ≤ s → hittingGenerator (inputWord n s) = encodeOutput (hittingList n s) ∧ (hittingList n s).dimension ≤ 256 * (n + s + 1) ^ 10 ∧ (encodeOutput (hittingList n s)).length ≤ PolynomialBounds.outputConstant * (n + s + 1) ^ 104 ∧ Hits s (hittingList n s)

End-to-end specification of the polynomial-time rational hitting-list generator: hittingGenerator is computable in polynomial time on a multi-tape Turing machine, and on every unary input inputWord n s with 1 ≤ n and 1 ≤ s it emits the canonical binary encoding of hittingList n s, which has dimension at most 256 * (n + s + 1) ^ 10, encoding length at most outputConstant * (n + s + 1) ^ 104, and hits every admissible nonzero formula in n variables with at most s nodes.