feat(Circuit): prove Lupanov upper bound by SamuelSchlesinger · Pull Request #890 · leanprover/cslib

SamuelSchlesinger · 2026-09-10T02:27:13Z

Add Boolean synthesis with sharing and prove the uniform (1 + ε) 2^n/n upper bound for De Morgan circuits.

Assisted by Codex, adapted from https://github.com/samuelSchlesinger/algebraic-circuits.

Add Boolean synthesis with sharing and prove the uniform (1 + ε) 2^n/n upper bound for De Morgan circuits.

crei · 2026-09-10T13:13:07Z

+variable {n : ℕ} {ι : Type u}
+
+/-- Functions available on the input or gate wires of a program. -/
+def available (p : Σ g, Program signature n g) : Set (BooleanFunction n) :=


I'm a bit confused by the sum type here, also in Synthesis.
What about the following:

/-- Functions available on the input or gate wires of a program. -/ def available {g : Nat} (p : Program signature n g) : Set (BooleanFunction n) := {f | ∃ w, ∀ x, p.trace interpretation x w = f x} /-- At most `cost` additional gates suffice to compute `targets` from `sources`, while preserving all functions already available in the starting program. -/ def Synthesis (sources targets : Set (BooleanFunction n)) (cost : ℕ) : Prop := ∀ g₁ (p₁ : Program _ _ g₁), sources ⊆ available p₁ → ∃ g₂, ∃ (p₂ : Program _ _ g₂), g₂ ≤ g₁ + cost ∧ available p₁ ⊆ available p₂ ∧ targets ⊆ available p₂

Maybe Program could also have a function that returns its gate count (even if it is part of the type) - then we would not need g₁ and g₂?

Adopted your definition. The ∃ g₂ stays since the gate count is a type index, but available now takes a Program directly and is just Set.range (p.wireFunction interpretation).

crei · 2026-09-10T13:15:31Z

+def available (p : Σ g, Program signature n g) : Set (BooleanFunction n) :=
+  {f | ∃ w, ∀ x, p.2.trace interpretation x w = f x}
+
+/-- At most `cost` additional gates suffice to compute `targets` from `sources`, while


This docstring reads super compressed and the definition is rather tricky. Maybe it's better to spell out the exact definition in english terms than trying to simplify it?

Rewrote the docstring to spell out the quantifier structure and why the starting program is arbitrary. Module doc expanded likewise.

crei · 2026-09-10T15:24:01Z

+/-!
+# Lupanov's block construction
+
+Split the truth table into address rows and data columns, and divide the rows into blocks.


Could you also explain what the purpose of this file is and not just what it does?

Rewrote the module doc to lead with the purpose of the file, then the truth-table picture, then where the gate count comes from. Lupanov.lean got a matching section on the parameter choice.

Address review on leanprover#890: - `available` takes a `Program` directly and is the range of `Program.wireFunction`; `Synthesis` quantifies over the gate count explicitly instead of through a sigma type. - Spell out the `Synthesis` definition in its docstring and expand the module doc. - Add `mem_available` and `inputs_subset_available`, and reuse the latter in `Synthesis.exists_circuit` and the test. - Add `Program.fanInAtMost_two` and `Circuit.fanInAtMost_two`, and state the fan-in bound in the Boolean module doc. - Remove the now-unused sigma-pair remark from the circuit module doc.

Address review on leanprover#890: - Lead the construction module doc with the purpose of the file, the truth-table picture (address rows, data columns, blocks, patterns, and the `left`/`right` split), and where the `2 ^ n / s` leading term comes from; add docstrings and section headers for every declaration. - Explain the parameter choice `k = 3 log n`, `d = n - 3 log n`, `s = n - 5 log n` in the asymptotic module doc and document each lemma's contribution to the argument. - Wrap two over-long declaration headers.

crei · 2026-09-11T08:07:38Z

+
+/-- `left` is true exactly at inputs whose address is a row of the block, at an offset where
+the pattern is `1`. -/
+private theorem left_eq_true (block : ℕ) (pattern : Assignment s) (x : Assignment (k + d)) :


Maybe move these closer to the definition so that the meaning is clear earlier on?

Moved left_eq_true and right_eq_true directly after their respective definitions.

crei · 2026-09-11T08:14:29Z

+open Filter
+
+/-- Polynomials are eventually dominated by `2 ^ n`. -/
+private theorem polynomial_le_pow (c r : ℕ) :


If mathlib does not have this, this should go into some very fundamental foundations library in cslib and be very public :)

Added public Nat.eventually_mul_pow_le_pow in Foundations/Data/Nat/Asymptotics.lean, using Mathlib’s existing little-o result and generalizing to natural bases greater than one.

crei · 2026-09-11T08:15:08Z

+  exact_mod_cast (by simpa using hn : (c : ℝ) * n ^ r ≤ (2 : ℝ) ^ n)
+
+/-- Any constant multiple of `log₂ n` is eventually at most `n`. -/
+private theorem log_le (c : ℕ) : ∀ᶠ n : ℕ in atTop, c * Nat.log 2 n ≤ n := by


Same with this.

Moved this alongside the polynomial bound as public Nat.eventually_mul_log_le, with a Nat.eventually_mul_log2_le corollary used here.

crei · 2026-09-11T08:21:23Z

+minterms, the per-pattern overhead of every block (`left` parts, constants, conjunctions and
+ORs), and the final constant. -/
+private theorem bound_le (n : ℕ) (hn : 5 * Nat.log 2 n < n) :
+    bound (3 * Nat.log 2 n) (n - 3 * Nat.log 2 n) (n - 5 * Nat.log 2 n) ≤


Could use Nat.log2 throughout here, it might make it a bit more readable.

Switched the asymptotic file to Nat.log2 and its corresponding lemmas.

crei · 2026-09-11T08:26:06Z

+  let k := 3 * l
+  let d := n - 3 * l
+  let s := n - 5 * l
+  let B := 2 ^ k / s + 1


Should be lowercase, but I assume this is the letter chose in the exposition, right?

Renamed it to blockCount.

crei · 2026-09-11T08:26:40Z

+  let d := n - 3 * l
+  let s := n - 5 * l
+  let B := 2 ^ k / s + 1
+  have hn0 : 0 < n := by omega


I wonder if some of these could be removed and replaced by grind at the place where they are used.

Removed the five routine opening facts and used grind where needed, keeping the main estimates named for readability.

crei

Great contribution, I would only request some minor changes.

feat(Circuit): prove Lupanov upper bound

6966c8e

Add Boolean synthesis with sharing and prove the uniform (1 + ε) 2^n/n upper bound for De Morgan circuits.

SamuelSchlesinger requested review from arademaker, chenson2018, fmontesi, kim-em and sorrachai as code owners September 10, 2026 02:27

SamuelSchlesinger requested a review from crei September 10, 2026 02:27

crei reviewed Sep 10, 2026

View reviewed changes

Comment thread Cslib/Computability/Circuit/Boolean/Basic.lean

crei reviewed Sep 10, 2026

View reviewed changes

Comment thread Cslib/Computability/Circuit/Boolean/LupanovConstruction.lean

SamuelSchlesinger added 2 commits September 10, 2026 11:42

crei reviewed Sep 11, 2026

View reviewed changes

crei requested changes Sep 11, 2026

View reviewed changes

refactor(Circuit): extract reusable asymptotic bounds

5a1cedb

Uh oh!

Conversation

SamuelSchlesinger commented Sep 10, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

crei left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants