Unrestricted depth-three lower bound: core

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/Core.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.Clause (V : Type uDepth1) : Type uDepth1

A finite set of signed input literals, interpreted as a disjunction.

Equations

• Complexity.DepthThreeLowerBound.Clause V = Finset (Complexity.DepthThreeLowerBound.Literal V)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.CNF (V : Type uDepth2) : Type uDepth2

A list of clauses, interpreted as a conjunction.

Equations

• Complexity.DepthThreeLowerBound.CNF V = List (Complexity.DepthThreeLowerBound.Clause V)

def Complexity.DepthThreeLowerBound.Literal.compl {V : Type uDepth3} (l : Literal V) : Literal V

Flip the satisfying value of a literal.

Equations

• l.compl = (l.1, !l.2)

@[simp]

theorem Complexity.DepthThreeLowerBound.Literal.eval_eq_true {V : Type uDepth3} (l : Literal V) (x : Cube V) : l.eval x = true ↔ x l.1 = l.2

@[simp]

theorem Complexity.DepthThreeLowerBound.Literal.compl_compl {V : Type uDepth3} (l : Literal V) : l.compl.compl = l

@[simp]

theorem Complexity.DepthThreeLowerBound.Literal.eval_compl {V : Type uDepth3} (l : Literal V) (x : Cube V) : l.compl.eval x = !l.eval x

noncomputable def Complexity.DepthThreeLowerBound.Clause.eval {V : Type uDepth3} (C : Clause V) (x : Cube V) : Bool

Evaluate the disjunction of the literals in a clause.

Equations

• C.eval x = decide (∃ l ∈ C, l.eval x = true)

noncomputable def Complexity.DepthThreeLowerBound.Clause.scope {V : Type uDepth3} (C : Clause V) : Finset V

The variables appearing in a clause, forgetting signs.

Equations

• C.scope = Finset.image Prod.fst C

noncomputable def Complexity.DepthThreeLowerBound.Clause.width {V : Type uDepth3} (C : Clause V) : ℕ

The number of distinct variables appearing in a clause.

Equations

• C.width = C.scope.card

def Complexity.DepthThreeLowerBound.Clause.Normalized {V : Type uDepth3} (C : Clause V) : Prop

No variable occurs with both signs in the clause.

Equations

• C.Normalized = ∀ (v : V), (v, false) ∈ C → (v, true) ∈ C → False

@[simp]

theorem Complexity.DepthThreeLowerBound.Clause.eval_eq_true {V : Type uDepth3} (C : Clause V) (x : Cube V) : C.eval x = true ↔ ∃ l ∈ C, x l.1 = l.2

@[simp]

theorem Complexity.DepthThreeLowerBound.Clause.eval_empty {V : Type uDepth3} (x : Cube V) : ∅.eval x = false

@[simp]

theorem Complexity.DepthThreeLowerBound.Clause.scope_empty {V : Type uDepth3} : ∅.scope = ∅

@[simp]

theorem Complexity.DepthThreeLowerBound.Clause.width_empty {V : Type uDepth3} : ∅.width = 0

@[simp]

theorem Complexity.DepthThreeLowerBound.Clause.eval_singleton {V : Type uDepth3} (l : Literal V) (x : Cube V) : {l}.eval x = l.eval x

theorem Complexity.DepthThreeLowerBound.Clause.eval_mono {V : Type uDepth3} {C D : Clause V} (h : C ⊆ D) {x : Cube V} (hx : C.eval x = true) : D.eval x = true

theorem Complexity.DepthThreeLowerBound.Clause.Normalized.subset {V : Type uDepth3} {C D : Clause V} (hD : D.Normalized) (h : C ⊆ D) : C.Normalized

theorem Complexity.DepthThreeLowerBound.Clause.Normalized.fst_injOn {V : Type uDepth3} {C : Clause V} (h : C.Normalized) : Set.InjOn Prod.fst ↑C

theorem Complexity.DepthThreeLowerBound.Clause.Normalized.card_eq_width {V : Type uDepth3} {C : Clause V} (h : C.Normalized) : Finset.card C = C.width

theorem Complexity.DepthThreeLowerBound.Clause.scope_mono {V : Type uDepth3} {C D : Clause V} (h : C ⊆ D) : C.scope ⊆ D.scope

theorem Complexity.DepthThreeLowerBound.Clause.width_mono {V : Type uDepth3} {C D : Clause V} (h : C ⊆ D) : C.width ≤ D.width

noncomputable def Complexity.DepthThreeLowerBound.CNF.eval {V : Type uDepth3} (H : CNF V) (x : Cube V) : Bool

Evaluate the conjunction of the clauses in a CNF.

Equations

• H.eval x = decide (∀ C ∈ H, C.eval x = true)

def Complexity.DepthThreeLowerBound.CNF.WidthAtMost {V : Type uDepth3} (H : CNF V) (b : ℕ) : Prop

Every clause involves at most the given number of distinct variables.

Equations

• H.WidthAtMost b = ∀ C ∈ H, C.width ≤ b

def Complexity.DepthThreeLowerBound.CNF.Normalized {V : Type uDepth3} (H : CNF V) : Prop

Every clause has at most one sign for each variable.

Equations

• H.Normalized = ∀ C ∈ H, C.Normalized

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.eval_eq_true {V : Type uDepth3} (H : CNF V) (x : Cube V) : H.eval x = true ↔ ∀ C ∈ H, C.eval x = true

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.eval_nil {V : Type uDepth3} (x : Cube V) : eval [] x = true

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.eval_cons {V : Type uDepth3} (C : Clause V) (H : CNF V) (x : Cube V) : eval (C :: H) x = (C.eval x && H.eval x)

@[simp]

theorem Complexity.DepthThreeLowerBound.CNF.eval_append {V : Type uDepth3} (H J : CNF V) (x : Cube V) : (H ++ J).eval x = (H.eval x && J.eval x)

theorem Complexity.DepthThreeLowerBound.CNF.eval_antitone {V : Type uDepth3} {H J : CNF V} (h : H ⊆ J) {x : Cube V} (hx : J.eval x = true) : H.eval x = true

theorem Complexity.DepthThreeLowerBound.CNF.WidthAtMost.mono {V : Type uDepth3} {H : CNF V} {b c : ℕ} (h : H.WidthAtMost b) (hbc : b ≤ c) : H.WidthAtMost c

def Complexity.DepthThreeLowerBound.indicator (b : Bool) : ℝ

The zero-one real indicator of a Boolean value.

Equations

• Complexity.DepthThreeLowerBound.indicator b = if b = true then 1 else 0

def Complexity.DepthThreeLowerBound.sign (b : Bool) : ℝ

Encode true by 1 and false by -1.

Equations

• Complexity.DepthThreeLowerBound.sign b = if b = true then 1 else -1

@[simp]

theorem Complexity.DepthThreeLowerBound.indicator_false : indicator false = 0

@[simp]

theorem Complexity.DepthThreeLowerBound.indicator_true : indicator true = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.sign_false : sign false = -1

@[simp]

theorem Complexity.DepthThreeLowerBound.sign_true : sign true = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.indicator_and (b c : Bool) : indicator (b && c) = indicator b * indicator c

theorem Complexity.DepthThreeLowerBound.indicator_nonneg (b : Bool) : 0 ≤ indicator b

theorem Complexity.DepthThreeLowerBound.indicator_le_one (b : Bool) : indicator b ≤ 1