Unrestricted depth-three lower bound: sparse partition

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

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

theorem Complexity.DepthThreeLowerBound.sparse_entropy_sum_budget (b m : ℕ) (η : ℝ) (hb : 1 ≤ b) (hη : 0 < η) (r F : ℕ → ℕ) (hF0 : F 0 = 0) (hF1 : F 1 = 0) (hbound : ∀ (i : ℕ), 2 ≤ i → i ≤ b → ↑(F i) * binaryEntropy (1 / ↑(r i)) ≤ η / ↑b) : ∑ i : Fin (b + 1), ↑(F ↑i * m) * binaryEntropy (1 / ↑(r ↑i)) ≤ η * ↑m

structure Complexity.DepthThreeLowerBound.SparsePartition {V : Type u} [Fintype V] (H : CNF V) (b M : ℕ) (η : ℝ) : Type u

A finite partition into sparse CNF leaves with the required evaluation identity.

• count : ℕ

  Number of pieces in the sparse partition.

• piece : Fin self.count → CNF V

  The sparse CNF at each partition index.

• normalized (i : Fin self.count) : (self.piece i).Normalized
• width_le (i : Fin self.count) : (self.piece i).WidthAtMost b
• clauses_le (i : Fin self.count) : List.length (self.piece i) ≤ M * Fintype.card V
• disjoint (i j : Fin self.count) : i ≠ j → ∀ (x : Cube V), ¬((self.piece i).eval x = true ∧ (self.piece j).eval x = true)
• indicator_eq_sum (x : Cube V) : indicator (H.eval x) = ∑ i : Fin self.count, indicator ((self.piece i).eval x)
• count_le : ↑self.count ≤ 2 ^ (η * ↑(Fintype.card V))

theorem Complexity.DepthThreeLowerBound.exists_sparse_partition_constant (b : ℕ) (η : ℝ) (hb : 1 ≤ b) (hη : 0 < η) : ∃ (M : ℕ), 0 < M ∧ ∀ (V : Type u) [inst : Fintype V] [DecidableEq V] (H : CNF V), H.WidthAtMost b → Nonempty (SparsePartition H b M η)