Unrestricted depth-three lower bound: sparse branch

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

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

def Complexity.DepthThreeLowerBound.sparseBatchUpdate {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) : Finset (Clause V)

Insert a batch of clauses and remove clauses it subsumes.

Equations

• Complexity.DepthThreeLowerBound.sparseBatchUpdate A B = B ∪ {C ∈ A | ¬∃ D ∈ B, D ⊆ C}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_sparseBatchUpdate {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {A B : Finset (Clause V)} {C : Clause V} : C ∈ sparseBatchUpdate A B ↔ C ∈ B ∨ C ∈ A ∧ ¬∃ D ∈ B, D ⊆ C

theorem Complexity.DepthThreeLowerBound.batch_subset_sparseBatchUpdate {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) : B ⊆ sparseBatchUpdate A B

theorem Complexity.DepthThreeLowerBound.sparseBatchUpdate_subset_union {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) : sparseBatchUpdate A B ⊆ B ∪ A

theorem Complexity.DepthThreeLowerBound.sparseBatchUpdate_mono_left {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {A A' B : Finset (Clause V)} (h : A ⊆ A') : sparseBatchUpdate A B ⊆ sparseBatchUpdate A' B

theorem Complexity.DepthThreeLowerBound.sparseBatchUpdate_dominates {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) {C : Clause V} (hC : C ∈ A) : ∃ D ∈ sparseBatchUpdate A B, D ⊆ C

theorem Complexity.DepthThreeLowerBound.sparseBatchUpdate_satisfies {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (A B : Finset (Clause V)) (x : Cube V) : (∀ C ∈ sparseBatchUpdate A B, C.eval x = true) ↔ (∀ C ∈ A, C.eval x = true) ∧ ∀ D ∈ B, D.eval x = true

structure Complexity.DepthThreeLowerBound.SparseState (V : Type uDepth2) : Type uDepth2

Active clauses together with the clauses introduced by sparsification.

• active : Finset (Clause V)

  The currently active clauses.

• side : Finset (Literal V)

  Side clauses accumulated during branching.

• added : Finset (Clause V)

  Clauses introduced by the sparsification process.

noncomputable def Complexity.DepthThreeLowerBound.SparseState.toCNF {V : Type uDepth1} (s : SparseState V) : CNF V

Read the active clause family as a CNF.

Equations

• s.toCNF = s.active.toList ++ List.map (fun (l : Complexity.DepthThreeLowerBound.Literal V) => {l}) s.side.toList

noncomputable def Complexity.DepthThreeLowerBound.SparseState.eval {V : Type uDepth1} (s : SparseState V) (x : Cube V) : Bool

Evaluate the CNF represented by a sparsification state.

Equations

• s.eval x = s.toCNF.eval x

structure Complexity.DepthThreeLowerBound.SparseState.Valid {V : Type uDepth1} (s : SparseState V) (b : ℕ) : Prop

The normalization, width, and containment invariants of a sparsification state.

• normalized (C : Clause V) : C ∈ s.active → C.Normalized
• nonempty (C : Clause V) : C ∈ s.active → Finset.Nonempty C
• antichain (C : Clause V) : C ∈ s.active → ∀ D ∈ s.active, C ⊆ D → C = D
• width_le (C : Clause V) : C ∈ s.active → C.width ≤ b
• added_subset : s.added ⊆ s.active

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseState.eval_eq_true {V : Type uDepth1} (s : SparseState V) (x : Cube V) : s.eval x = true ↔ (∀ C ∈ s.active, C.eval x = true) ∧ ∀ l ∈ s.side, l.eval x = true

def Complexity.DepthThreeLowerBound.SparseState.batchUpdate {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (s : SparseState V) (B : Finset (Clause V)) : SparseState V

Update both active and introduced clauses with an insertion batch.

Equations

• s.batchUpdate B = { active := Complexity.DepthThreeLowerBound.sparseBatchUpdate s.active B, side := s.side, added := Complexity.DepthThreeLowerBound.sparseBatchUpdate s.added B }

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseState.batchUpdate_active {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (s : SparseState V) (B : Finset (Clause V)) : (s.batchUpdate B).active = sparseBatchUpdate s.active B

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseState.batchUpdate_side {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (s : SparseState V) (B : Finset (Clause V)) : (s.batchUpdate B).side = s.side

@[simp]

theorem Complexity.DepthThreeLowerBound.SparseState.batchUpdate_added {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (s : SparseState V) (B : Finset (Clause V)) : (s.batchUpdate B).added = sparseBatchUpdate s.added B

theorem Complexity.DepthThreeLowerBound.SparseState.eval_batchUpdate_eq_true {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (s : SparseState V) (B : Finset (Clause V)) (x : Cube V) : (s.batchUpdate B).eval x = true ↔ s.eval x = true ∧ ∀ C ∈ B, C.eval x = true

structure Complexity.DepthThreeLowerBound.InsertionBatch {V : Type uDepth1} (s : SparseState V) (i : ℕ) : Type uDepth1

A uniform batch of fresh clauses used in a sparsification step.

• clauses : Finset (Clause V)

  The clauses inserted by this batch.

• size : ℕ

  The common size of the selected clauses.

• nonempty : self.clauses.Nonempty
• size_pos : 0 < self.size
• size_lt : self.size < i
• uniform (D : Clause V) : D ∈ self.clauses → Finset.card D = self.size
• subclause (D : Clause V) : D ∈ self.clauses → ∃ A ∈ s.active, D ⊂ A
• pairwise_disjoint (D : Clause V) : D ∈ self.clauses → ∀ E ∈ self.clauses, D ≠ E → Disjoint D E

theorem Complexity.DepthThreeLowerBound.InsertionBatch.clause_nonempty {V : Type uDepth1} {s : SparseState V} {i : ℕ} (B : InsertionBatch s i) (D : Clause V) (hD : D ∈ B.clauses) : Finset.Nonempty D

theorem Complexity.DepthThreeLowerBound.InsertionBatch.antichain {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i : ℕ} (B : InsertionBatch s i) (D : Clause V) : D ∈ B.clauses → ∀ E ∈ B.clauses, D ⊆ E → D = E

theorem Complexity.DepthThreeLowerBound.InsertionBatch.fresh {V : Type uDepth1} {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) (D : Clause V) : D ∈ B.clauses → ∀ A ∈ s.active, ¬A ⊆ D

theorem Complexity.DepthThreeLowerBound.InsertionBatch.not_mem_active {V : Type uDepth1} {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) {D : Clause V} (hD : D ∈ B.clauses) : D ∉ s.active

theorem Complexity.DepthThreeLowerBound.InsertionBatch.disjoint_active {V : Type uDepth1} {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) : Disjoint s.active B.clauses

theorem Complexity.DepthThreeLowerBound.InsertionBatch.disjoint_added {V : Type uDepth1} {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) : Disjoint s.added B.clauses

theorem Complexity.DepthThreeLowerBound.InsertionBatch.removed_strict {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) {C : Clause V} (hC : C ∈ s.active) (hnot : C ∉ sparseBatchUpdate s.active B.clauses) : ∃ D ∈ B.clauses, D ⊂ C

theorem Complexity.DepthThreeLowerBound.InsertionBatch.normalized {V : Type uDepth1} {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) {D : Clause V} (hD : D ∈ B.clauses) : D.Normalized

theorem Complexity.DepthThreeLowerBound.InsertionBatch.width_le {V : Type uDepth1} {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) {D : Clause V} (hD : D ∈ B.clauses) : D.width ≤ b

theorem Complexity.DepthThreeLowerBound.InsertionBatch.valid_batchUpdate {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i b : ℕ} (B : InsertionBatch s i) (hs : s.Valid b) : (s.batchUpdate B.clauses).Valid b

theorem Complexity.DepthThreeLowerBound.InsertionBatch.literal_occurrences_le_one {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i : ℕ} (B : InsertionBatch s i) (u : ℕ) (l : Literal V) : literalOccurrences B.clauses u l ≤ 1

@[simp]

theorem Complexity.DepthThreeLowerBound.InsertionBatch.added_eq {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i : ℕ} (B : InsertionBatch s i) : (s.batchUpdate B.clauses).added = sparseBatchUpdate s.added B.clauses

structure Complexity.DepthThreeLowerBound.SignedSunflower {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (s : SparseState V) (i r : ℕ) : Type uDepth1

A uniform signed-clause sunflower selected from the active family.

• family : Finset (Clause V)

  The selected family of sunflower clauses.

• core : Clause V

  The common intersection of the sunflower.

• subset_active : self.family ⊆ s.active
• card_family : self.family.card = r
• two_le : 2 ≤ r
• uniform (A : Clause V) : A ∈ self.family → Finset.card A = i
• core_nonempty : Finset.Nonempty self.core
• sunflower : Sunflower self.family self.core

theorem Complexity.DepthThreeLowerBound.SignedSunflower.card_family_ge_two {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : 2 ≤ f.family.card

theorem Complexity.DepthThreeLowerBound.SignedSunflower.family_nonempty {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : f.family.Nonempty

theorem Complexity.DepthThreeLowerBound.SignedSunflower.size_ge_two {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : 2 ≤ i

theorem Complexity.DepthThreeLowerBound.SignedSunflower.size_le {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r b : ℕ} (f : SignedSunflower s i r) (hs : s.Valid b) : i ≤ b

def Complexity.DepthThreeLowerBound.SignedSunflower.petals {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : Finset (Clause V)

The sunflower clauses with their common core removed.

Equations

• f.petals = Finset.image (fun (A : Complexity.DepthThreeLowerBound.Clause V) => A \ f.core) f.family

@[simp]

theorem Complexity.DepthThreeLowerBound.SignedSunflower.mem_petals {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (D : Clause V) : D ∈ f.petals ↔ ∃ A ∈ f.family, A \ f.core = D

def Complexity.DepthThreeLowerBound.SignedSunflower.coreBatch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : InsertionBatch s i

The insertion batch for the sunflower's core branch.

Equations

• f.coreBatch = { clauses := {f.core}, size := Finset.card f.core, nonempty := ⋯, size_pos := ⋯, size_lt := ⋯, uniform := ⋯, subclause := ⋯, pairwise_disjoint := ⋯ }

def Complexity.DepthThreeLowerBound.SignedSunflower.petalBatch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : InsertionBatch s i

The insertion batch for the sunflower's petal branch.

Equations

• f.petalBatch = { clauses := f.petals, size := i - Finset.card f.core, nonempty := ⋯, size_pos := ⋯, size_lt := ⋯, uniform := ⋯, subclause := ⋯, pairwise_disjoint := ⋯ }

def Complexity.DepthThreeLowerBound.SignedSunflower.batch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (choice : Bool) : InsertionBatch s i

Choose the core or petal insertion batch.

Equations

• f.batch choice = if choice = true then f.petalBatch else f.coreBatch

def Complexity.DepthThreeLowerBound.SignedSunflower.coreBranch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : SparseState V

The sparsification state obtained by taking the core branch.

Equations

• f.coreBranch = s.batchUpdate f.coreBatch.clauses

def Complexity.DepthThreeLowerBound.SignedSunflower.petalBranch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) : SparseState V

The sparsification state obtained by taking the petal branch.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DepthThreeLowerBound.SignedSunflower.branch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (choice : Bool) : SparseState V

Choose the core or petal successor state.

Equations

• f.branch choice = if choice = true then f.petalBranch else f.coreBranch

@[simp]

theorem Complexity.DepthThreeLowerBound.SignedSunflower.branch_active {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (choice : Bool) : (f.branch choice).active = sparseBatchUpdate s.active (f.batch choice).clauses

@[simp]

theorem Complexity.DepthThreeLowerBound.SignedSunflower.branch_added {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (choice : Bool) : (f.branch choice).added = sparseBatchUpdate s.added (f.batch choice).clauses

theorem Complexity.DepthThreeLowerBound.SignedSunflower.batch_card {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (choice : Bool) : (f.batch choice).clauses.card = if choice = true then r else 1

theorem Complexity.DepthThreeLowerBound.SignedSunflower.coreBranch_valid {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r b : ℕ} (f : SignedSunflower s i r) (hs : s.Valid b) : f.coreBranch.Valid b

theorem Complexity.DepthThreeLowerBound.SignedSunflower.petalBranch_valid {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r b : ℕ} (f : SignedSunflower s i r) (hs : s.Valid b) : f.petalBranch.Valid b

theorem Complexity.DepthThreeLowerBound.SignedSunflower.branch_valid {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r b : ℕ} (f : SignedSunflower s i r) (choice : Bool) (hs : s.Valid b) : (f.branch choice).Valid b

theorem Complexity.DepthThreeLowerBound.SignedSunflower.core_false_iff_complement_units {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (C : Clause V) (x : Cube V) : C.eval x = false ↔ ∀ l ∈ Finset.image Literal.compl C, l.eval x = true

theorem Complexity.DepthThreeLowerBound.SignedSunflower.petals_true_of_core_false {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (x : Cube V) (hA : ∀ C ∈ s.active, C.eval x = true) (hC : f.core.eval x = false) (P : Clause V) : P ∈ f.petals → P.eval x = true

theorem Complexity.DepthThreeLowerBound.SignedSunflower.eval_coreBranch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (x : Cube V) : f.coreBranch.eval x = (s.eval x && f.core.eval x)

theorem Complexity.DepthThreeLowerBound.SignedSunflower.eval_petalBranch {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (x : Cube V) : f.petalBranch.eval x = (s.eval x && !f.core.eval x)

theorem Complexity.DepthThreeLowerBound.SignedSunflower.branch_indicator {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (x : Cube V) : indicator (s.eval x) = indicator (f.coreBranch.eval x) + indicator (f.petalBranch.eval x)

theorem Complexity.DepthThreeLowerBound.SignedSunflower.branch_disjoint {V : Type uDepth1} [instDecidableEqV : DecidableEq V] {s : SparseState V} {i r : ℕ} (f : SignedSunflower s i r) (x : Cube V) : ¬(f.coreBranch.eval x = true ∧ f.petalBranch.eval x = true)