Unrestricted depth-three lower bound: sparse prefix

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

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

structure Complexity.DepthThreeLowerBound.SparseNumerics (r e D : ℕ → ℕ) (b : ℕ) : Prop

Numerical hypotheses for the occurrence bounds in sparsification.

• r_ge_two (i : ℕ) : 2 ≤ i → i ≤ b → 2 ≤ r i
• e_one : e 1 = 1
• e_succ (i : ℕ) : 1 ≤ i → i + 1 ≤ b → e (i + 1) = i.factorial * (r (i + 1) - 1) ^ i
• D_eq (i : ℕ) : 1 ≤ i → i ≤ b → D i = (e i + 1) * (2 + ∑ v ∈ Finset.Ico 1 i, D v)

theorem Complexity.DepthThreeLowerBound.sparse_occurrence_le_of_no_sunflower {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} (hnum : SparseNumerics r e D b) (s : SparseState V) (u : ℕ) (hu : 1 ≤ u) (hub : u ≤ b) (hno : ¬Nonempty (SignedSunflower s u (r u))) (l : Literal V) : literalOccurrences s.active u l ≤ e u

structure Complexity.DepthThreeLowerBound.SparseStep {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (s t : SparseState V) : Type uDepth1

A minimal eligible sunflower, a branch choice, and its resulting state.

• size : ℕ

  The common size of the selected clauses.

• selected : SignedSunflower s self.size (r self.size)

  The selected signed sunflower.

• minimal (j : ℕ) : 2 ≤ j → j < self.size → ¬Nonempty (SignedSunflower s j (r j))
• choice : Bool

  Choose the core branch or the petal branch.

• target : t = self.selected.branch self.choice

noncomputable def Complexity.DepthThreeLowerBound.SparseStep.batch {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} (step : SparseStep r s t) : InsertionBatch s step.size

The insertion batch selected by a sparsification step.

Equations

• step.batch = step.selected.batch step.choice

theorem Complexity.DepthThreeLowerBound.SparseStep.target_active {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} (step : SparseStep r s t) : t.active = sparseBatchUpdate s.active step.batch.clauses

theorem Complexity.DepthThreeLowerBound.SparseStep.target_added {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} (step : SparseStep r s t) : t.added = sparseBatchUpdate s.added step.batch.clauses

theorem Complexity.DepthThreeLowerBound.SparseStep.valid {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} {b : ℕ} (step : SparseStep r s t) (hs : s.Valid b) : t.Valid b

theorem Complexity.DepthThreeLowerBound.SparseStep.fresh_added {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} {b : ℕ} (step : SparseStep r s t) (hs : s.Valid b) : Disjoint s.added step.batch.clauses

theorem Complexity.DepthThreeLowerBound.SparseStep.batch_size_count {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} (step : SparseStep r s t) (u : ℕ) : (clausesOfSize step.batch.clauses u).card = if step.batch.size = u then step.batch.clauses.card else 0

theorem Complexity.DepthThreeLowerBound.SparseStep.removed_eq_empty_of_le {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} {b : ℕ} (step : SparseStep r s t) (hs : s.Valid b) (u : ℕ) (hu : u ≤ step.batch.size) : subsumedOfSize s.added step.batch.clauses u = ∅

theorem Complexity.DepthThreeLowerBound.SparseStep.update_balance {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s t : SparseState V} {b : ℕ} (step : SparseStep r s t) (hs : s.Valid b) (u : ℕ) : (clausesOfSize t.added u).card + (subsumedOfSize s.added step.batch.clauses u).card = (clausesOfSize s.added u).card + if step.batch.size = u then step.batch.clauses.card else 0

inductive Complexity.DepthThreeLowerBound.SparsePath {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (start : SparseState V) : SparseState V → Type uDepth1

A finite sequence of valid sparsification steps.

• nil {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start : SparseState V} : SparsePath r start start
• snoc {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start s t : SparseState V} (path : SparsePath r start s) (step : SparseStep r s t) : SparsePath r start t

def Complexity.DepthThreeLowerBound.SparsePath.length {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start finish : SparseState V} : SparsePath r start finish → ℕ

The number of steps in a sparsification path.

Equations

• Complexity.DepthThreeLowerBound.SparsePath.nil.length = 0
• (path.snoc step).length = path.length + 1

noncomputable def Complexity.DepthThreeLowerBound.SparsePath.insertions {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start finish : SparseState V} : SparsePath r start finish → ℕ → ℕ

The clauses inserted along a sparsification path.

Equations

• Complexity.DepthThreeLowerBound.SparsePath.nil.insertions x✝ = 0
• (path.snoc step).insertions x✝ = path.insertions x✝ + if step.batch.size = x✝ then step.batch.clauses.card else 0

def Complexity.DepthThreeLowerBound.SparsePath.processed {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start finish : SparseState V} : SparsePath r start finish → ℕ → ℕ

Count processed sunflowers of each size along the path.

Equations

• Complexity.DepthThreeLowerBound.SparsePath.nil.processed x✝ = 0
• (path.snoc step).processed x✝ = path.processed x✝ + if step.size = x✝ then 1 else 0

def Complexity.DepthThreeLowerBound.SparsePath.petalSteps {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start finish : SparseState V} : SparsePath r start finish → ℕ → ℕ

Count petal-branch choices of each size along the path.

Equations

• Complexity.DepthThreeLowerBound.SparsePath.nil.petalSteps x✝ = 0
• (path.snoc step).petalSteps x✝ = path.petalSteps x✝ + if step.size = x✝ ∧ step.choice = true then 1 else 0

theorem Complexity.DepthThreeLowerBound.SparsePath.valid {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} (path : SparsePath r start finish) (hstart : start.Valid b) : finish.Valid b

@[simp]

theorem Complexity.DepthThreeLowerBound.SparsePath.insertions_nil {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start : SparseState V} (u : ℕ) : nil.insertions u = 0

@[simp]

theorem Complexity.DepthThreeLowerBound.SparsePath.insertions_snoc {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start s t : SparseState V} (path : SparsePath r start s) (step : SparseStep r s t) (u : ℕ) : (path.snoc step).insertions u = path.insertions u + if step.batch.size = u then step.batch.clauses.card else 0

theorem Complexity.DepthThreeLowerBound.SparsePath.insertions_sum_snoc {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start s t : SparseState V} (path : SparsePath r start s) (step : SparseStep r s t) (u : ℕ) : ∑ v ∈ Finset.Ico 1 u, (path.snoc step).insertions v = ∑ v ∈ Finset.Ico 1 u, path.insertions v + if step.batch.size < u then step.batch.clauses.card else 0

theorem Complexity.DepthThreeLowerBound.SparsePath.added_occurrence_bound {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) (u : ℕ) : 1 ≤ u → u ≤ b → ∀ (l : Literal V), literalOccurrences finish.added u l ≤ e u + 1

theorem Complexity.DepthThreeLowerBound.SparsePath.online_insertion_bound {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) (u : ℕ) : 1 ≤ u → u ≤ b → path.insertions u ≤ (clausesOfSize finish.added u).card + (e u + 1) * ∑ v ∈ Finset.Ico 1 u, path.insertions v

theorem Complexity.DepthThreeLowerBound.SparsePath.insertion_recurrence {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} [Fintype V] (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) (u : ℕ) (hu : 1 ≤ u) (hub : u ≤ b) : path.insertions u ≤ (e u + 1) * (2 * Fintype.card V + ∑ v ∈ Finset.Ico 1 u, path.insertions v)

theorem Complexity.DepthThreeLowerBound.SparsePath.length_le_insertions {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} (path : SparsePath r start finish) (hstart : start.Valid b) : path.length ≤ ∑ u ∈ Finset.Ico 1 b, path.insertions u

theorem Complexity.DepthThreeLowerBound.SparsePath.processed_le_insertions {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start finish : SparseState V} (path : SparsePath r start finish) (i : ℕ) : path.processed i ≤ ∑ u ∈ Finset.Ico 1 i, path.insertions u

theorem Complexity.DepthThreeLowerBound.SparsePath.petalSteps_mul_le_insertions {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start finish : SparseState V} (path : SparsePath r start finish) (i : ℕ) : r i * path.petalSteps i ≤ ∑ u ∈ Finset.Ico 1 i, path.insertions u

theorem Complexity.DepthThreeLowerBound.sparse_insertion_budget_of_recurrence (r e D N : ℕ → ℕ) (b m : ℕ) (hnum : SparseNumerics r e D b) (hN : ∀ (u : ℕ), 1 ≤ u → u ≤ b → N u ≤ (e u + 1) * (2 * m + ∑ v ∈ Finset.Ico 1 u, N v)) (u : ℕ) : 1 ≤ u → u ≤ b → N u ≤ D u * m

theorem Complexity.DepthThreeLowerBound.SparsePath.insertion_budget {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} [Fintype V] (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) (u : ℕ) (hu : 1 ≤ u) (hub : u ≤ b) : path.insertions u ≤ D u * Fintype.card V

theorem Complexity.DepthThreeLowerBound.SparsePath.insertion_sum_budget {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} [Fintype V] (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) (i : ℕ) (hi : i ≤ b + 1) : ∑ u ∈ Finset.Ico 1 i, path.insertions u ≤ (∑ u ∈ Finset.Ico 1 i, D u) * Fintype.card V

theorem Complexity.DepthThreeLowerBound.SparsePath.length_budget {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} [Fintype V] (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) : path.length ≤ (∑ u ∈ Finset.Ico 1 b, D u) * Fintype.card V

theorem Complexity.DepthThreeLowerBound.SparsePath.processed_budget {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} [Fintype V] (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) (i : ℕ) (hi : i ≤ b) : path.processed i ≤ (∑ u ∈ Finset.Ico 1 i, D u) * Fintype.card V

theorem Complexity.DepthThreeLowerBound.SparsePath.petalSteps_budget {V : Type uDepth1} [DecidableEq V] {r e D : ℕ → ℕ} {b : ℕ} {start finish : SparseState V} [Fintype V] (path : SparsePath r start finish) (hnum : SparseNumerics r e D b) (hstart : start.Valid b) (hadded : start.added = ∅) (i : ℕ) (hi : i ≤ b) : r i * path.petalSteps i ≤ (∑ u ∈ Finset.Ico 1 i, D u) * Fintype.card V