Unrestricted depth-three lower bound: sparse tree

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

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

def Complexity.DepthThreeLowerBound.SparseEligible {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (s : SparseState V) : Prop

There exists an eligible sunflower in the current state.

Equations

• Complexity.DepthThreeLowerBound.SparseEligible r s = ∃ (i : ℕ), Nonempty (Complexity.DepthThreeLowerBound.SignedSunflower s i (r i))

def Complexity.DepthThreeLowerBound.SparseTerminal {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (s : SparseState V) : Prop

There is no eligible sunflower left in the current state.

Equations

• Complexity.DepthThreeLowerBound.SparseTerminal r s = ∀ (i : ℕ), ¬Nonempty (Complexity.DepthThreeLowerBound.SignedSunflower s i (r i))

theorem Complexity.DepthThreeLowerBound.sparseTerminal_of_not_eligible {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s : SparseState V} (h : ¬SparseEligible r s) : SparseTerminal r s

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

A smallest eligible sunflower selected for branching.

• 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))

noncomputable def Complexity.DepthThreeLowerBound.sparseSelect {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (s : SparseState V) (h : SparseEligible r s) : SparseSelection r s

Choose a smallest eligible sunflower when one exists.

Equations

• Complexity.DepthThreeLowerBound.sparseSelect r s h = { size := Nat.find h, selected := Classical.choice ⋯, minimal := ⋯ }

def Complexity.DepthThreeLowerBound.SparseSelection.branch {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s : SparseState V} (c : SparseSelection r s) (choice : Bool) : SparseState V

The successor state selected by the Boolean branch choice.

Equations

• c.branch choice = c.selected.branch choice

def Complexity.DepthThreeLowerBound.SparseSelection.step {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s : SparseState V} (c : SparseSelection r s) (choice : Bool) : SparseStep r s (c.branch choice)

The certified sparsification step determined by a selected branch.

Equations

• c.step choice = { size := c.size, selected := c.selected, minimal := ⋯, choice := choice, target := ⋯ }

def Complexity.DepthThreeLowerBound.SparseSelection.label {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s : SparseState V} {b : ℕ} (c : SparseSelection r s) (hs : s.Valid b) : Fin (b + 1)

The clause-size label attached to a selected sunflower.

Equations

• c.label hs = ⟨c.size, ⋯⟩

theorem Complexity.DepthThreeLowerBound.SparseSelection.branch_valid {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s : SparseState V} {b : ℕ} (c : SparseSelection r s) (hs : s.Valid b) (choice : Bool) : (c.branch choice).Valid b

theorem Complexity.DepthThreeLowerBound.SparseSelection.branch_eval_imp {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {s : SparseState V} (c : SparseSelection r s) (choice : Bool) (x : Cube V) (h : (c.branch choice).eval x = true) : s.eval x = true

def Complexity.DepthThreeLowerBound.SparsePath.prepend {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start middle : SparseState V} (step : SparseStep r start middle) {finish : SparseState V} : SparsePath r middle finish → SparsePath r start finish

Prepend one step to a sparsification path.

Equations

• Complexity.DepthThreeLowerBound.SparsePath.prepend step Complexity.DepthThreeLowerBound.SparsePath.nil = Complexity.DepthThreeLowerBound.SparsePath.nil.snoc step
• Complexity.DepthThreeLowerBound.SparsePath.prepend step (path.snoc next) = (Complexity.DepthThreeLowerBound.SparsePath.prepend step path).snoc next

theorem Complexity.DepthThreeLowerBound.SparsePath.length_prepend {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start middle finish : SparseState V} (step : SparseStep r start middle) (path : SparsePath r middle finish) : (prepend step path).length = 1 + path.length

theorem Complexity.DepthThreeLowerBound.SparsePath.processed_prepend {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start middle finish : SparseState V} (step : SparseStep r start middle) (path : SparsePath r middle finish) (i : ℕ) : (prepend step path).processed i = (if step.size = i then 1 else 0) + path.processed i

theorem Complexity.DepthThreeLowerBound.SparsePath.petalSteps_prepend {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {start middle finish : SparseState V} (step : SparseStep r start middle) (path : SparsePath r middle finish) (i : ℕ) : (prepend step path).petalSteps i = (if step.size = i ∧ step.choice = true then 1 else 0) + path.petalSteps i

structure Complexity.DepthThreeLowerBound.SparseTreeResult {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (b : ℕ) (start : SparseState V) (fuel : ℕ) : Type uDepth1

A finite sparsification tree with valid paths and terminal leaves.

• tree : SparseDecisionTree (Fin (b + 1))

  The binary sparsification decision tree.

• finish : self.tree.Leaf → SparseState V

  The final state at each leaf.

• path (p : self.tree.Leaf) : SparsePath r start (self.finish p)

  The sequence of sparsification steps leading to each leaf.

• terminal_or_exhausted (p : self.tree.Leaf) : SparseTerminal r (self.finish p) ∨ (self.path p).length = fuel
• stream_length (p : self.tree.Leaf) (i : Fin (b + 1)) : (self.tree.stream p i).length = (self.path p).processed ↑i
• stream_ones (p : self.tree.Leaf) (i : Fin (b + 1)) : List.count true (self.tree.stream p i) = (self.path p).petalSteps ↑i
• leaf_eval_imp (p : self.tree.Leaf) (x : Cube V) : (self.finish p).eval x = true → start.eval x = true
• indicator_eq_sum (x : Cube V) : indicator (start.eval x) = ∑ p : self.tree.Leaf, indicator ((self.finish p).eval x)
• disjoint (p q : self.tree.Leaf) : p ≠ q → ∀ (x : Cube V), ¬((self.finish p).eval x = true ∧ (self.finish q).eval x = true)

def Complexity.DepthThreeLowerBound.SparseTreeResult.stop {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (b : ℕ) (s : SparseState V) (fuel : ℕ) (h : SparseTerminal r s ∨ fuel = 0) : SparseTreeResult r b s fuel

Construct a leaf tree when the current sparsification state is terminal.

Equations

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

def Complexity.DepthThreeLowerBound.SparseTreeResult.join {V : Type uDepth1} [DecidableEq V] {r : ℕ → ℕ} {b fuel : ℕ} {s : SparseState V} (c : SparseSelection r s) (hs : s.Valid b) (left : SparseTreeResult r b (c.branch false) fuel) (right : SparseTreeResult r b (c.branch true) fuel) : SparseTreeResult r b s (fuel + 1)

Join the two branch trees below a selected sunflower.

Equations

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

def Complexity.DepthThreeLowerBound.SparseTreeResult.build {V : Type uDepth1} [DecidableEq V] (r : ℕ → ℕ) (b fuel : ℕ) (s : SparseState V) : s.Valid b → SparseTreeResult r b s fuel

Build a sparsification tree recursively within the supplied fuel bound.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.SparseTreeResult.build r b 0 x x_1 = Complexity.DepthThreeLowerBound.SparseTreeResult.stop r b x 0 ⋯

def Complexity.DepthThreeLowerBound.sparseTreeFuel {V : Type uDepth1} [Fintype V] (D : ℕ → ℕ) (b : ℕ) : ℕ

A sufficient fuel bound for finite-width sparsification.

Equations

• Complexity.DepthThreeLowerBound.sparseTreeFuel D b = (∑ u ∈ Finset.Ico 1 b, D u) * Fintype.card V

noncomputable def Complexity.DepthThreeLowerBound.sparseTree {V : Type uDepth1} [DecidableEq V] [Fintype V] (r D : ℕ → ℕ) (b : ℕ) (s : SparseState V) (hs : s.Valid b) : SparseTreeResult r b s (sparseTreeFuel D b)

The complete sparsification tree from an initial state.

Equations

• Complexity.DepthThreeLowerBound.sparseTree r D b s hs = Complexity.DepthThreeLowerBound.SparseTreeResult.build r b (Complexity.DepthThreeLowerBound.sparseTreeFuel D b) s hs

theorem Complexity.DepthThreeLowerBound.sparseTree_terminal {V : Type uDepth1} [DecidableEq V] [Fintype V] {r e D : ℕ → ℕ} {b : ℕ} (hnum : SparseNumerics r e D b) (s : SparseState V) (hs : s.Valid b) (hadded : s.added = ∅) (p : (sparseTree r D b s hs).tree.Leaf) : SparseTerminal r ((sparseTree r D b s hs).finish p)

theorem Complexity.DepthThreeLowerBound.sparseTree_stream_length {V : Type uDepth1} [DecidableEq V] [Fintype V] {r e D : ℕ → ℕ} {b : ℕ} (hnum : SparseNumerics r e D b) (s : SparseState V) (hs : s.Valid b) (hadded : s.added = ∅) (p : (sparseTree r D b s hs).tree.Leaf) (i : Fin (b + 1)) : ((sparseTree r D b s hs).tree.stream p i).length ≤ (∑ u ∈ Finset.Ico 1 ↑i, D u) * Fintype.card V

theorem Complexity.DepthThreeLowerBound.sparseTree_stream_ones {V : Type uDepth1} [DecidableEq V] [Fintype V] {r e D : ℕ → ℕ} {b : ℕ} (hnum : SparseNumerics r e D b) (s : SparseState V) (hs : s.Valid b) (hadded : s.added = ∅) (p : (sparseTree r D b s hs).tree.Leaf) (i : Fin (b + 1)) : r ↑i * List.count true ((sparseTree r D b s hs).tree.stream p i) ≤ (∑ u ∈ Finset.Ico 1 ↑i, D u) * Fintype.card V