Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.SparseLeafCNF

Unrestricted depth-three lower bound: sparse leaf cnf #

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

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

source
def Complexity.DepthThreeLowerBound.SparseNormalization.toState {V : Type uDepth1} {H : CNF V} {b : ℕ} (N : SparseNormalization H b) :
SparseState V

Convert a normalized sparse family to its initial sparsification state.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.SparseNormalization.toState_valid {V : Type uDepth1} {H : CNF V} {b : ℕ} (N : SparseNormalization H b) :
    N.toState.Valid b
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.SparseNormalization.toState_added {V : Type uDepth1} {H : CNF V} {b : ℕ} (N : SparseNormalization H b) :
    N.toState.added = ∅
    source
    theorem Complexity.DepthThreeLowerBound.SparseNormalization.toState_eval {V : Type uDepth1} {H : CNF V} {b : ℕ} (N : SparseNormalization H b) (x : Cube V) :
    N.toState.eval x = H.eval x
    source
    theorem Complexity.DepthThreeLowerBound.SparseState.toCNF_normalized {V : Type uDepth1} (s : SparseState V) {b : ℕ} (hs : s.Valid b) :
    s.toCNF.Normalized
    source
    theorem Complexity.DepthThreeLowerBound.SparseState.toCNF_widthAtMost {V : Type uDepth1} (s : SparseState V) {b : ℕ} (hs : s.Valid b) (hb : 1 ≤ b) :
    s.toCNF.WidthAtMost b
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.SparseState.toCNF_length {V : Type uDepth1} (s : SparseState V) :
    List.length s.toCNF = s.active.card + s.side.card
    source
    theorem Complexity.DepthThreeLowerBound.SparseState.active_card_eq_sum_sizes {V : Type uDepth1} (s : SparseState V) {b : ℕ} (hs : s.Valid b) :
    s.active.card = ∑ u ∈ Finset.Icc 1 b, (clausesOfSize s.active u).card
    source
    theorem Complexity.DepthThreeLowerBound.SparseState.active_card_le_of_terminal {V : Type uDepth1} [instDecidableEqV : DecidableEq V] [Fintype V] (s : SparseState V) {r e D : ℕ → ℕ} {b : ℕ} (hs : s.Valid b) (hnum : SparseNumerics r e D b) (hterminal : ∀ (i : ℕ), ¬Nonempty (SignedSunflower s i (r i))) :
    s.active.card ≤ 2 * Fintype.card V * ∑ u ∈ Finset.Icc 1 b, e u
    source
    theorem Complexity.DepthThreeLowerBound.SparseState.toCNF_length_le_of_terminal {V : Type uDepth1} [instDecidableEqV : DecidableEq V] [Fintype V] (s : SparseState V) {r e D : ℕ → ℕ} {b : ℕ} (hs : s.Valid b) (hnum : SparseNumerics r e D b) (hterminal : ∀ (i : ℕ), ¬Nonempty (SignedSunflower s i (r i))) :
    List.length s.toCNF ≤ (2 + 2 * ∑ u ∈ Finset.Icc 1 b, e u) * Fintype.card V