Unrestricted depth-three lower bound: sparse test codes

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/SparseTestCodes.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.SparseClauseCode (V : Type uDepth1) (b : ℕ) : Type uDepth1

A finite encoding of a sparse clause.

Equations

• Complexity.DepthThreeLowerBound.SparseClauseCode V b = (Fin b → Option (Complexity.DepthThreeLowerBound.Literal V))

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.SparseTestCode (V : Type uDepth2) (b L : ℕ) : Type uDepth2

A finite encoding of a sparse CNF test.

Equations

• Complexity.DepthThreeLowerBound.SparseTestCode V b L = (Fin L → Option (Complexity.DepthThreeLowerBound.SparseClauseCode V b))

noncomputable def Complexity.DepthThreeLowerBound.SparseClauseCode.decode {V : Type uDepth3} [Fintype V] {b : ℕ} (c : SparseClauseCode V b) : Clause V

Decode a sparse clause code to its set of literals.

Equations

• c.decode = {l : Complexity.DepthThreeLowerBound.Literal V | ∃ (i : Fin b), c i = some l}

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseClauseCode.mem_decode {V : Type uDepth4} [Fintype V] {b : ℕ} (c : SparseClauseCode V b) (l : Literal V) : l ∈ c.decode ↔ ∃ (i : Fin b), c i = some l

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseClauseCode.decode_none {V : Type uDepth5} [Fintype V] (b : ℕ) : (decode fun (x : Fin b) => none) = ∅

theorem Complexity.DepthThreeLowerBound.SparseClauseCode.exists_decode_of_card_le {V : Type uDepth6} [Fintype V] (C : Clause V) {b : ℕ} (hC : Finset.card C ≤ b) : ∃ (c : SparseClauseCode V b), c.decode = C

theorem Complexity.DepthThreeLowerBound.SparseClauseCode.exists_decode_of_normalized {V : Type uDepth7} [Fintype V] (C : Clause V) {b : ℕ} (hn : C.Normalized) (hw : C.width ≤ b) : ∃ (c : SparseClauseCode V b), c.decode = C

theorem Complexity.DepthThreeLowerBound.SparseClauseCode.card_eq {V : Type uDepth8} [Fintype V] (b : ℕ) : Fintype.card (SparseClauseCode V b) = (2 * Fintype.card V + 1) ^ b

def Complexity.DepthThreeLowerBound.SparseTestCode.decode {V : Type uDepth9} [Fintype V] {b L : ℕ} : SparseTestCode V b L → CNF V

Decode a sparse test code to its CNF.

Equations

• One or more equations did not get rendered due to their size.
• x_2.decode = []

noncomputable def Complexity.DepthThreeLowerBound.SparseTestCode.eval {V : Type uDepth10} [Fintype V] {b L : ℕ} (c : SparseTestCode V b L) (x : Cube V) : Bool

Evaluate the CNF decoded from a sparse test code.

Equations

• c.eval x = c.decode.eval x

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseTestCode.decode_cons_none {V : Type uDepth11} [Fintype V] {b L : ℕ} (c : SparseTestCode V b L) : decode (Fin.cons none c) = c.decode

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseTestCode.decode_cons_some {V : Type uDepth12} [Fintype V] {b L : ℕ} (d : SparseClauseCode V b) (c : SparseTestCode V b L) : decode (Fin.cons (some d) c) = d.decode :: c.decode

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseTestCode.decode_none {V : Type uDepth13} [Fintype V] (b L : ℕ) : (decode fun (x : Fin L) => none) = []

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseTestCode.eval_none {V : Type uDepth14} [Fintype V] (b L : ℕ) (x : Cube V) : eval (fun (x : Fin L) => none) x = true

theorem Complexity.DepthThreeLowerBound.SparseTestCode.eval_cons_empty {V : Type uDepth15} [Fintype V] {b L : ℕ} (c : SparseTestCode V b L) (x : Cube V) : eval (Fin.cons (some fun (x : Fin b) => none) c) x = false

theorem Complexity.DepthThreeLowerBound.SparseTestCode.exists_decode_of_normalized {V : Type uDepth16} [Fintype V] (H : CNF V) (b L : ℕ) : H.Normalized → H.WidthAtMost b → List.length H ≤ L → ∃ (c : SparseTestCode V b L), c.decode = H

theorem Complexity.DepthThreeLowerBound.SparseTestCode.exists_eval_eq {V : Type uDepth17} [Fintype V] (H : CNF V) {b L : ℕ} (hw : H.WidthAtMost b) (hlen : List.length H ≤ L) : ∃ (c : SparseTestCode V b L), ∀ (x : Cube V), c.eval x = H.eval x

theorem Complexity.DepthThreeLowerBound.SparseTestCode.card_eq {V : Type uDepth18} [Fintype V] (b L : ℕ) : Fintype.card (SparseTestCode V b L) = ((2 * Fintype.card V + 1) ^ b + 1) ^ L