feat(circuit): linear-size Boolean and two-element arithmetic simulation

CslibFrontier.lean

@@ -1079,6 +1079,7 @@ public import CslibFrontier.Computability.Circuit.Arithmetic.SetMultilinearLower
 public import CslibFrontier.Computability.Circuit.Arithmetic.SetMultilinearize
 public import CslibFrontier.Computability.Circuit.Arithmetic.SigmaPi
 public import CslibFrontier.Computability.Circuit.Arithmetic.SumFlatten
+public import CslibFrontier.Computability.Circuit.Arithmetic.Synthesis
 public import CslibFrontier.Computability.Circuit.Arithmetic.VNP
 public import CslibFrontier.Computability.Circuit.Arithmetic.VP
 public import CslibFrontier.Computability.Circuit.Arithmetic.Waring
@@ -1123,6 +1124,7 @@ public import CslibFrontier.Computability.Circuit.Boolean.AffineDisperserCore.Re
 public import CslibFrontier.Computability.Circuit.Boolean.AffineDisperserCore.State
 public import CslibFrontier.Computability.Circuit.Boolean.AltFormula
 public import CslibFrontier.Computability.Circuit.Boolean.AltFormula.TopDown
+public import CslibFrontier.Computability.Circuit.Boolean.Arithmetic
 public import CslibFrontier.Computability.Circuit.Boolean.AtLeast
 public import CslibFrontier.Computability.Circuit.Boolean.BalancedCode
 public import CslibFrontier.Computability.Circuit.Boolean.Barrington

CslibFrontier/Computability/Circuit/Arithmetic/MatrixMultiplication/Exponent.lean

@@ -11,7 +11,7 @@ public import CslibFrontier.Computability.Circuit.Arithmetic
 public import CslibFrontier.Foundations.LinearAlgebra.Tensor.Basic
 public import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import CslibFrontier.Computability.Circuit.Synthesis
-import CslibFrontier.Computability.Circuit.Arithmetic.VP
+import CslibFrontier.Computability.Circuit.Arithmetic.Synthesis
 import CslibFrontier.Computability.Circuit.Inputization
 
 /-!

CslibFrontier/Computability/Circuit/Arithmetic/Synthesis.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger, Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger, Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import CslibFrontier.Computability.Circuit.Arithmetic
+public import Cslib.Computability.Circuit.Synthesis
+import Mathlib.Data.Fin.VecNotation
+
+/-!
+# Synthesis over the arithmetic basis
+
+Constants, sums and products can be synthesized over an arithmetic signature without importing
+polynomial families, degree bounds or projections. The constant symbols have arbitrary type
+`K` and are interpreted in a carrier `R` by a supplied map. The primitive rules need only
+addition and multiplication on `R`; the finite-sum rule needs an additive commutative monoid.
+There is no semiring assumption on `K`.
+
+The declarations retain their names, statements and proofs from the VP module. VP publicly
+imports this module, while value-level clients can import it directly.
+
+## Main results
+
+* `Cslib.Circuits.Synthesis.arith_const`: a constant costs one gate.
+* `Cslib.Circuits.Synthesis.arith_add`: adding two available functions costs one gate.
+* `Cslib.Circuits.Synthesis.arith_mul`: multiplying two available functions costs one gate.
+* `Cslib.Circuits.Synthesis.arith_sum`: synthesize a finite sum from its summands and zero.
+-/
+
+public section
+
+namespace Cslib.Circuits
+
+universe u
+
+variable {K : Type u} {n : ℕ}
+variable {R : Type*} {constant : K → R} {s : Set ((Fin n → R) → R)} {f g : (Fin n → R) → R}
+
+/-- A constant costs one gate. -/
+theorem Synthesis.arith_const [Add R] [Mul R] (a : K) :
+    Synthesis (arithInterpretationWith K constant) s {fun _ => constant a} 1 :=
+  Synthesis.gate (σ := arithSignature K) (.const a) (fun i => Fin.elim0 i) (fun i => Fin.elim0 i)
+
+/-- The sum of two available functions costs one gate. -/
+theorem Synthesis.arith_add [Add R] [Mul R] (hf : f ∈ s) (hg : g ∈ s) :
+    Synthesis (arithInterpretationWith K constant) s {fun x => f x + g x} 1 :=
+  Synthesis.gate (σ := arithSignature K) .add ![f, g] fun i => by fin_cases i <;> assumption
+
+/-- The product of two available functions costs one gate. -/
+theorem Synthesis.arith_mul [Add R] [Mul R] (hf : f ∈ s) (hg : g ∈ s) :
+    Synthesis (arithInterpretationWith K constant) s {fun x => f x * g x} 1 :=
+  Synthesis.gate (σ := arithSignature K) .mul ![f, g] fun i => by fin_cases i <;> assumption
+
+/-- A finite sum costs its summands and one addition each, when zero is available. -/
+theorem Synthesis.arith_sum {ι : Type*} [AddCommMonoid R] [Mul R] (indices : Finset ι)
+    (summand : ι → (Fin n → R) → R) (cost : ι → ℕ) (hzero : (fun _ => 0) ∈ s)
+    (h : ∀ i ∈ indices, Synthesis (arithInterpretationWith K constant) s {summand i} (cost i)) :
+    Synthesis (arithInterpretationWith K constant) s {fun x => ∑ i ∈ indices, summand i x}
+      (∑ i ∈ indices, (cost i + 1)) := by
+  have := Synthesis.finset_fold (· + ·) 1 (fun f g => Synthesis.arith_add (Set.mem_insert f {g})
+    (Set.mem_insert_of_mem f rfl)) indices (Synthesis.of_mem hzero) h
+  simpa only [Finset.sum_eq_fold, Nat.add_zero] using this
+
+end Cslib.Circuits

CslibFrontier/Computability/Circuit/Arithmetic/VP.lean

@@ -9,7 +9,7 @@ module
 
 public import CslibFrontier.Computability.Circuit.Arithmetic
 public import CslibFrontier.Computability.Circuit.Pi
-public import Cslib.Computability.Circuit.Synthesis
+public import CslibFrontier.Computability.Circuit.Arithmetic.Synthesis
 public import Cslib.Foundations.Data.Nat.PolynomialBound
 public import Mathlib.Algebra.MvPolynomial.Degrees
 import CslibFrontier.Foundations.Data.MvPolynomial.Substitution
@@ -50,6 +50,11 @@ variable of `Q` a variable of `P` or a constant. A family `f` is a *p-projection
 `f n` is a projection of `g (t n)` for a polynomially bounded `t`. Projections are Valiant's
 reductions; `VP` is closed under them.
 
+Generic arithmetic synthesis rules are publicly re-exported from
+`CslibFrontier.Computability.Circuit.Arithmetic.Synthesis`; value-level clients need not import
+the polynomial-family API. The polynomial synthesis rule `Synthesis.exists_circuit_polynomial`
+remains here.
+
 ## Main definitions
 
 * `Cslib.Circuits.Circuit.polynomial`: the formal polynomial computed by an arithmetic circuit.
@@ -71,9 +76,6 @@ reductions; `VP` is closed under them.
 * `Cslib.Circuits.Arithmetic.IsProjection.trans`,
   `Cslib.Circuits.Arithmetic.PolynomialFamily.IsPProjection.trans`: projections compose.
 * `Cslib.Circuits.Arithmetic.totalDegree_projection_le`: projections do not raise the degree.
-* `Cslib.Circuits.Synthesis.arith_const`, `Cslib.Circuits.Synthesis.arith_add`,
-  `Cslib.Circuits.Synthesis.arith_mul`, `Cslib.Circuits.Synthesis.arith_sum`: synthesis rules for
-  arithmetic circuits.
 * `Cslib.Circuits.Synthesis.exists_circuit_polynomial`: a synthesis bound gives a circuit computing
   the polynomial.
 * `Cslib.Circuits.Arithmetic.VP.of_isPProjection`: `VP` is closed under p-projections.
@@ -135,40 +137,7 @@ with evaluating the circuit under `arithInterpretation K`. -/
   simpa [MvPolynomial.aeval_def, MvPolynomial.eval₂_id, arithInterpretation] using
     c.aeval_polynomial x j
 
-/-! ### Synthesis of arithmetic circuits -/
-
-section Synthesis
-
-variable {R : Type*} {constant : K → R} {s : Set ((Fin n → R) → R)} {f g : (Fin n → R) → R}
-
-omit [CommSemiring K] in
-/-- A constant costs one gate. -/
-theorem Synthesis.arith_const [Add R] [Mul R] (a : K) :
-    Synthesis (arithInterpretationWith K constant) s {fun _ => constant a} 1 :=
-  Synthesis.gate (σ := arithSignature K) (.const a) (fun i => Fin.elim0 i) (fun i => Fin.elim0 i)
-
-omit [CommSemiring K] in
-/-- The sum of two available functions costs one gate. -/
-theorem Synthesis.arith_add [Add R] [Mul R] (hf : f ∈ s) (hg : g ∈ s) :
-    Synthesis (arithInterpretationWith K constant) s {fun x => f x + g x} 1 :=
-  Synthesis.gate (σ := arithSignature K) .add ![f, g] fun i => by fin_cases i <;> assumption
-
-omit [CommSemiring K] in
-/-- The product of two available functions costs one gate. -/
-theorem Synthesis.arith_mul [Add R] [Mul R] (hf : f ∈ s) (hg : g ∈ s) :
-    Synthesis (arithInterpretationWith K constant) s {fun x => f x * g x} 1 :=
-  Synthesis.gate (σ := arithSignature K) .mul ![f, g] fun i => by fin_cases i <;> assumption
-
-omit [CommSemiring K] in
-/-- A finite sum costs its summands and one addition each, when zero is available. -/
-theorem Synthesis.arith_sum {ι : Type*} [AddCommMonoid R] [Mul R] (indices : Finset ι)
-    (summand : ι → (Fin n → R) → R) (cost : ι → ℕ) (hzero : (fun _ => 0) ∈ s)
-    (h : ∀ i ∈ indices, Synthesis (arithInterpretationWith K constant) s {summand i} (cost i)) :
-    Synthesis (arithInterpretationWith K constant) s {fun x => ∑ i ∈ indices, summand i x}
-      (∑ i ∈ indices, (cost i + 1)) := by
-  have := Synthesis.finset_fold (· + ·) 1 (fun f g => Synthesis.arith_add (Set.mem_insert f {g})
-    (Set.mem_insert_of_mem f rfl)) indices (Synthesis.of_mem hzero) h
-  simpa only [Finset.sum_eq_fold, Nat.add_zero] using this
+/-! ### Synthesis of formal polynomials -/
 
 /-- A synthesis bound on a function `F` from the inputs gives a circuit, within the bound,
 computing the polynomial `F X`. -/
@@ -179,8 +148,6 @@ theorem Synthesis.exists_circuit_polynomial
   obtain ⟨c, hc, hsize⟩ := h.exists_circuit
   exact ⟨c, congrFun (hc X) 0, hsize⟩
 
-end Synthesis
-
 namespace Arithmetic
 
 /-- A family of polynomials over `K`: for every `n`, a polynomial `poly n` in `vars n`

CslibFrontier/Computability/Circuit/Boolean/Arithmetic.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import CslibFrontier.Computability.Circuit.Arithmetic
+public import Cslib.Computability.Circuit.Boolean.Basic
+public import Cslib.Computability.Circuit.Simulation
+public import Mathlib.Algebra.Ring.BooleanRing
+import CslibFrontier.Computability.Circuit.Arithmetic.Synthesis
+import CslibFrontier.Computability.Circuit.Boolean.Synthesis
+
+/-!
+# Boolean circuits and arithmetic over the two-element field
+
+Mathlib's `BooleanRing Bool` has addition XOR and multiplication AND. On that carrier,
+arithmetic circuits and De Morgan Boolean circuits simulate each other with uniform gate
+budgets three and four. The simulations preserve every output on every input, including
+zero-input and zero-output circuits. Size counts operation nodes, including constants;
+input and output wires are free. These are nonuniform existence and gate-size claims,
+not runtime bounds for a compiler or formal polynomial identities.
+
+This proves the two-element-field case of [Arora–Barak, web draft 2007-01-08,
+Chapter 14, Exercise 1, printed p. 265/PDF p. 281][AroraBarak07]. The exercise for arbitrary
+fixed finite fields additionally needs a representation of field elements by bits and is not
+claimed here. Existing generic gate replacement supplies the circuit-level simulation.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.arithmetic_simulates_boolean`: at most three arithmetic gates per
+  Boolean gate.
+* `Cslib.Circuits.Boolean.boolean_simulates_arithmetic`: at most four Boolean gates per
+  arithmetic gate.
+* `Cslib.Circuits.Boolean.exists_arithmetic_simulation`: all-output simulation with size factor
+  three.
+* `Cslib.Circuits.Boolean.exists_boolean_simulation`: all-output simulation with size factor
+  four.
+-/
+
+public section
+
+namespace Cslib.Circuits.Boolean
+
+open Synthesis
+
+private theorem arith_gate_synthesis (op : Op) :
+    Synthesis (arithInterpretation Bool) (inputs (signature.Arity op)) {interpretation op} 3 := by
+  cases op with
+  | const c =>
+    exact (Synthesis.arith_const (constant := id) c).mono
+      (Set.Subset.refl _) (Set.Subset.refl _) (by decide)
+  | not =>
+    have hx : Synthesis (arithInterpretation Bool) (inputs 1) {fun x => x 0} 0 :=
+      Synthesis.of_mem ⟨0, rfl⟩
+    have hc : Synthesis (arithInterpretation Bool) (inputs 1) {fun _ => true} 1 :=
+      Synthesis.arith_const (constant := id) true
+    have h := hx.binary hc ArithOp.add
+    have he : (fun x : Fin 1 → Bool => x 0 + true) = interpretation Op.not := by
+      funext x
+      simp [interpretation, Bool.add_eq_xor]
+    simp only [arithInterpretation, arithInterpretationWith, Fin.val_zero, ↓reduceIte,
+      Fin.val_one, Nat.one_ne_zero] at h
+    rw [he] at h
+    exact h.mono (Set.Subset.refl _) (Set.Subset.refl _) (by decide)
+  | and =>
+    have h : Synthesis (arithInterpretation Bool) (inputs 2) {fun x => x 0 * x 1} 1 :=
+      Synthesis.arith_mul (constant := id) ⟨0, rfl⟩ ⟨1, rfl⟩
+    exact h.mono (Set.Subset.refl _) (Set.Subset.refl _) (by decide)
+  | or =>
+    have hs : Synthesis (arithInterpretation Bool) (inputs 2) {fun x => x 0 + x 1} 1 :=
+      Synthesis.arith_add (constant := id) ⟨0, rfl⟩ ⟨1, rfl⟩
+    have hm : Synthesis (arithInterpretation Bool) (inputs 2) {fun x => x 0 * x 1} 1 :=
+      Synthesis.arith_mul (constant := id) ⟨0, rfl⟩ ⟨1, rfl⟩
+    have h := hs.binary hm ArithOp.add
+    have he : (fun x : Fin 2 → Bool => (x 0 + x 1) + x 0 * x 1) = interpretation Op.or := by
+      funext x
+      change (x 0 + x 1) + x 0 * x 1 = (x 0 || x 1)
+      cases x 0 <;> cases x 1 <;> rfl
+    simp only [arithInterpretation, arithInterpretationWith, Fin.val_zero, ↓reduceIte,
+      Fin.val_one, Nat.one_ne_zero] at h
+    rw [he] at h
+    exact h
+
+private theorem boolean_gate_synthesis (op : ArithOp Bool) :
+    Synthesis interpretation (inputs ((arithSignature Bool).Arity op))
+      {arithInterpretation Bool op} 4 := by
+  cases op with
+  | const c => exact (Synthesis.const c).mono (Set.Subset.refl _) (Set.Subset.refl _) (by decide)
+  | mul =>
+    have hx : Synthesis interpretation (inputs 2) {fun x => x 0} 0 :=
+      Synthesis.of_mem ⟨0, rfl⟩
+    have hy : Synthesis interpretation (inputs 2) {fun x => x 1} 0 :=
+      Synthesis.of_mem ⟨1, rfl⟩
+    exact (hx.and hy).mono (Set.Subset.refl _) (Set.Subset.refl _) (by decide)
+  | add =>
+    have hx : Synthesis interpretation (inputs 2) {fun x => x 0} 0 :=
+      Synthesis.of_mem ⟨0, rfl⟩
+    have hy : Synthesis interpretation (inputs 2) {fun x => x 1} 0 :=
+      Synthesis.of_mem ⟨1, rfl⟩
+    exact hx.xor hy
+
+/-- Each De Morgan gate is computed by at most three gates over the two-element arithmetic
+basis. NOT is `x + 1`; OR is `x + y + x * y`. -/
+theorem arithmetic_simulates_boolean :
+    (arithInterpretation Bool).SimulatesWithCost interpretation (fun _ => 3) :=
+  fun op => (arith_gate_synthesis op).exists_circuit
+
+/-- Each arithmetic gate over the two-element field is computed by at most four De Morgan
+gates. Addition uses the existing four-gate XOR synthesis. -/
+theorem boolean_simulates_arithmetic :
+    interpretation.SimulatesWithCost (arithInterpretation Bool) (fun _ => 4) :=
+  fun op => (boolean_gate_synthesis op).exists_circuit
+
+/-- A Boolean circuit has an equivalent two-element arithmetic circuit with at most three
+times its number of gates. Every designated output is preserved. -/
+theorem exists_arithmetic_simulation {n m : ℕ} (c : Circuit signature n m) :
+    ∃ d : Circuit (arithSignature Bool) n m,
+      d.eval (arithInterpretation Bool) = c.eval interpretation ∧ d.size ≤ 3 * c.size :=
+  c.exists_simulation_le arithmetic_simulates_boolean
+
+/-- A two-element arithmetic circuit has an equivalent Boolean circuit with at most four
+times its number of gates. Every designated output is preserved. -/
+theorem exists_boolean_simulation {n m : ℕ} (c : Circuit (arithSignature Bool) n m) :
+    ∃ d : Circuit signature n m,
+      d.eval interpretation = c.eval (arithInterpretation Bool) ∧ d.size ≤ 4 * c.size :=
+  c.exists_simulation_le boolean_simulates_arithmetic
+
+end Cslib.Circuits.Boolean

CslibFrontierResults/Entries.lean

@@ -29,6 +29,7 @@ import CslibFrontier.Computability.Circuit.Arithmetic.HittingSet.SetMultilinear
 import CslibFrontier.Computability.Circuit.Arithmetic.HittingSet.Sparse
 import CslibFrontier.Computability.Circuit.Arithmetic.HittingSet.SparseOrbit
 import CslibFrontier.Computability.Circuit.Arithmetic.MatrixMultiplication.NineQuarters
+import CslibFrontier.Computability.Circuit.Boolean.Arithmetic
 import CslibFrontier.Computability.Circuit.Boolean.BarringtonClass
 import CslibFrontier.Computability.Circuit.Boolean.Braverman.Fooling
 import CslibFrontier.Computability.Circuit.Boolean.Formula.Andreev
@@ -634,6 +635,23 @@ register_result "braverman" where
     than Braverman's; size and depth count NOT gates and constants; nonuniform and \
     information-theoretic."
 
+register_result "boolean-two-element-arithmetic-simulation" where
+  title := "Boolean and two-element arithmetic circuits have linearly related sizes"
+  topic := "circuit complexity"
+  sources := [
+    { paper := AroraBarak07, theorem := "Chapter 14, Exercise 1 (two-element case)",
+      locator := "Web draft 2007-01-08, printed p. 265; PDF p. 281" }
+  ]
+  theorems := [
+    Cslib.Circuits.Boolean.exists_arithmetic_simulation,
+    Cslib.Circuits.Boolean.exists_boolean_simulation
+  ]
+  scope := "Bool's Boolean ring, with XOR addition and AND multiplication. All outputs and \
+    all inputs are preserved; arithmetic simulates De Morgan circuits with size factor 3, \
+    and De Morgan circuits simulate arithmetic with factor 4. Constants count as gates; \
+    input/output wires are free. Nonuniform existence, not compiler runtime or formal \
+    polynomial equality. This does not complete the arbitrary fixed finite-field exercise."
+
 register_result "formal-complexity-measure-leaf-bound" where
   title := "Formal complexity measures lower-bound constant-free formula leaf size"
   topic := "circuit complexity"

CslibFrontierTests/ArithmeticSynthesis.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+-- upstream: candidate
+import CslibFrontier.Computability.Circuit.Arithmetic.Synthesis
+
+/-! # Arithmetic synthesis without polynomial families
+
+String-labelled constants need no semiring structure on the labels. Their interpretation here
+is string length in the natural numbers, exercising the topic module without importing VP.
+-/
+
+open Cslib.Circuits
+
+example : ∃ c : Circuit (arithSignature String) 0 1,
+    c.size ≤ 1 ∧ ∀ x, c.eval (arithInterpretationWith String String.length) x 0 = 5 := by
+  have h : Synthesis (arithInterpretationWith String String.length) (inputs 0) {fun _ => 5} 1 :=
+    Synthesis.arith_const "hello"
+  obtain ⟨c, hc, hs⟩ := h.exists_circuit
+  exact ⟨c, hs, fun x => congrFun (hc x) 0⟩