diff --git a/CslibFrontier.lean b/CslibFrontier.lean
index badd7db739..05fba3df4f 100644
--- a/CslibFrontier.lean
+++ b/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
diff --git a/CslibFrontier/Computability/Circuit/Arithmetic/MatrixMultiplication/Exponent.lean b/CslibFrontier/Computability/Circuit/Arithmetic/MatrixMultiplication/Exponent.lean
index 6ff32d4195..b76ff98eeb 100644
--- a/CslibFrontier/Computability/Circuit/Arithmetic/MatrixMultiplication/Exponent.lean
+++ b/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
 
 /-!
diff --git a/CslibFrontier/Computability/Circuit/Arithmetic/Synthesis.lean b/CslibFrontier/Computability/Circuit/Arithmetic/Synthesis.lean
new file mode 100644
index 0000000000..371bfbb9f2
--- /dev/null
+++ b/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
diff --git a/CslibFrontier/Computability/Circuit/Arithmetic/VP.lean b/CslibFrontier/Computability/Circuit/Arithmetic/VP.lean
index 2672e07b39..5934e875b3 100644
--- a/CslibFrontier/Computability/Circuit/Arithmetic/VP.lean
+++ b/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`
diff --git a/CslibFrontier/Computability/Circuit/Boolean/Arithmetic.lean b/CslibFrontier/Computability/Circuit/Boolean/Arithmetic.lean
new file mode 100644
index 0000000000..bff2810f74
--- /dev/null
+++ b/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
diff --git a/CslibFrontierResults/Entries.lean b/CslibFrontierResults/Entries.lean
index ac3a62f9b8..2f1c312df2 100644
--- a/CslibFrontierResults/Entries.lean
+++ b/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"
diff --git a/CslibFrontierTests/ArithmeticSynthesis.lean b/CslibFrontierTests/ArithmeticSynthesis.lean
new file mode 100644
index 0000000000..9d42f008f6
--- /dev/null
+++ b/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⟩
diff --git a/CslibFrontierTests/BooleanArithmetic.lean b/CslibFrontierTests/BooleanArithmetic.lean
new file mode 100644
index 0000000000..5503d9027a
--- /dev/null
+++ b/CslibFrontierTests/BooleanArithmetic.lean
@@ -0,0 +1,74 @@
+/-
+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.Boolean.Arithmetic
+import Cslib.Computability.Circuit.Composition
+import CslibFrontier.Computability.Circuit.Pi
+
+/-! # Two-element arithmetic/Boolean circuit clients
+
+Multiple outputs test preservation of XOR and AND together. Constant and pure-wiring clients
+exercise zero inputs and a zero gate budget. Arithmetic here means evaluation in Bool's
+Boolean ring, not polynomial equality.
+-/
+
+open Cslib.Circuits
+
+private def arithmeticPair : Circuit (arithSignature Bool) 2 2 :=
+  (Circuit.oneGate (σ := arithSignature Bool) ArithOp.add id).append
+    (Circuit.oneGate (σ := arithSignature Bool) ArithOp.mul id)
+
+example : ∃ d : Circuit Boolean.signature 2 2,
+    d.size ≤ 8 ∧ ∀ x, d.eval Boolean.interpretation x = ![x 0 ^^ x 1, x 0 && x 1] := by
+  obtain ⟨d, he, hs⟩ := Boolean.exists_boolean_simulation arithmeticPair
+  refine ⟨d, ?_, ?_⟩
+  · simpa [arithmeticPair] using hs
+  · intro x
+    rw [he]
+    ext i
+    fin_cases i <;> rfl
+
+private def booleanPair : Circuit Boolean.signature 2 2 :=
+  (Circuit.oneGate (σ := Boolean.signature) Boolean.Op.or id).append
+    (Circuit.oneGate (σ := Boolean.signature) Boolean.Op.not (fun _ => 0))
+
+example : ∃ d : Circuit (arithSignature Bool) 2 2,
+    d.size ≤ 6 ∧ ∀ x, d.eval (arithInterpretation Bool) x = ![x 0 || x 1, !(x 0)] := by
+  obtain ⟨d, he, hs⟩ := Boolean.exists_arithmetic_simulation booleanPair
+  refine ⟨d, ?_, ?_⟩
+  · simpa [booleanPair] using hs
+  · intro x
+    rw [he]
+    ext i
+    fin_cases i <;> rfl
+
+example : ∃ d : Circuit (arithSignature Bool) 0 1,
+    d.size ≤ 3 ∧ ∀ x, d.eval (arithInterpretation Bool) x 0 = true := by
+  obtain ⟨d, he, hs⟩ := Boolean.exists_arithmetic_simulation
+    (Circuit.oneGate (Boolean.Op.const true) Fin.elim0 : Circuit Boolean.signature 0 1)
+  refine ⟨d, hs, ?_⟩
+  intro x
+  rw [he]
+  rfl
+
+example : ∃ d : Circuit Boolean.signature 0 1,
+    d.size ≤ 4 ∧ ∀ x, d.eval Boolean.interpretation x 0 = false := by
+  obtain ⟨d, he, hs⟩ := Boolean.exists_boolean_simulation
+    (Circuit.oneGate (ArithOp.const false) Fin.elim0 : Circuit (arithSignature Bool) 0 1)
+  refine ⟨d, hs, ?_⟩
+  intro x
+  rw [he]
+  rfl
+
+example : ∃ d : Circuit (arithSignature Bool) 2 2,
+    d.size = 0 ∧ ∀ x, d.eval (arithInterpretation Bool) x = x := by
+  obtain ⟨d, he, hs⟩ := Boolean.exists_arithmetic_simulation
+    (Circuit.wiring Boolean.signature id : Circuit Boolean.signature 2 2)
+  refine ⟨d, Nat.eq_zero_of_le_zero hs, ?_⟩
+  intro x
+  rw [he]
+  rfl
diff --git a/manual/circuits-logic-and-other-models/algebraic-and-quantum.md b/manual/circuits-logic-and-other-models/algebraic-and-quantum.md
index fb72f0358c..a41fe4f84b 100644
--- a/manual/circuits-logic-and-other-models/algebraic-and-quantum.md
+++ b/manual/circuits-logic-and-other-models/algebraic-and-quantum.md
@@ -19,6 +19,41 @@ Theorem 14.7 should not be used as an unrestricted circuit-to-determinant specif
 linear dimension bound fails the existing repeated-squaring degree check. See the audit's
 [checked client](../../CslibFrontierTests/AroraBarakAlgebraic.lean) and exact model conventions.
 
+## Arithmetic synthesis without polynomial families
+
+Import [Arithmetic.Synthesis](../../CslibFrontier/Computability/Circuit/Arithmetic/Synthesis.lean)
+for `Synthesis.arith_const`, `arith_add`, `arith_mul` and `arith_sum`. The constant symbols
+have arbitrary type `K`, interpreted by a supplied map into the value carrier `R`; no semiring
+structure on `K` is required. The primitive rules need addition and multiplication on `R`,
+and the finite-sum rule needs an additive commutative monoid. VP publicly re-exports the same
+rules and names for existing clients; `Synthesis.exists_circuit_polynomial` stays in VP.
+
+The Boolean simulation below and the
+[matrix-multiplication exponent module](../../CslibFrontier/Computability/Circuit/Arithmetic/MatrixMultiplication/Exponent.lean)
+use the shared topic module directly. Run `scripts/build.sh CslibFrontierTests.ArithmeticSynthesis`
+for a [client](../../CslibFrontierTests/ArithmeticSynthesis.lean) that interprets string-labelled
+constants as natural-number lengths, without importing VP or giving the labels a semiring.
+
+## Boolean and two-element arithmetic circuits
+
+Import [Boolean.Arithmetic](../../CslibFrontier/Computability/Circuit/Boolean/Arithmetic.lean)
+for the two-element case of Arora–Barak's Chapter 14, Exercise 1. Mathlib's Boolean ring
+on `Bool` uses XOR for addition and AND for multiplication. `Boolean.exists_arithmetic_simulation c`
+replaces a De Morgan circuit by an arithmetic circuit on this same carrier, preserving every
+output with at most `3 * c.size` gates. `Boolean.exists_boolean_simulation c` goes the other way
+with at most `4 * c.size` gates. Constants count as gates; input/output wires are free, and
+zero-input and pure-wiring circuits are included.
+
+The `arithmetic_simulates_boolean` and `boolean_simulates_arithmetic` gate-budget certificates
+also work with the generic `Circuit.exists_simulationWithCost` API. These are circuit-value
+and nonuniform size results, not formal polynomial identities or certified translation runtimes.
+They establish the GF(2) milestone, not the exercise for every fixed finite field; the latter
+still needs bit encodings and the general-field directions. Existing `Synthesis.bitBlast`
+handles an equivalence to a fixed-width bit cube and should be reused where applicable.
+Run `scripts/build.sh CslibFrontierTests.BooleanArithmetic` for the
+[checked clients](../../CslibFrontierTests/BooleanArithmetic.lean): multiple XOR/AND and OR/NOT
+outputs, zero-input constants and zero-gate wiring.
+
 ## Valiant classes and term models
 
 [PolynomialFamily](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Circuit/Arithmetic/VP.lean#L188) stores a variable-count function and a polynomial at each family index, with no bounds. `PolynomialFamily.IsPFamily` requires the variable count and actual total degree to be polynomially bounded in the family index. `VP` additionally requires circuits of polynomially bounded size computing the family's formal polynomials. The class is nonuniform and includes degree as an independent restriction. The library's repeated-squaring example has small circuits but exponential degree and is therefore excluded from VP. A p-projection substitutes variables/constants and permits a polynomially bounded family reindexing.
diff --git a/results/arora-barak-2007.md b/results/arora-barak-2007.md
index f755337999..3986199e55 100644
--- a/results/arora-barak-2007.md
+++ b/results/arora-barak-2007.md
@@ -3,7 +3,8 @@
 Audit and checked client: Christian Reitwiessner, with Codex assistance.
 
 This is a growing statement-level audit under [#4711](https://github.com/cslib-community/cslib-frontier/issues/4711),
-not a completeness claim for the book or library. Its source is the
+not a completeness claim for the book or library. The scope includes exercises that establish
+new theory; routine practice is excluded. Its source is the
 [public web draft dated 2007-01-08](https://theory.cs.princeton.edu/complexity/book.pdf)
 (489 PDF pages; SHA-256 `da0881782a35bde6a0779a2eb1a8d480f39fbddf70bbb92824d1dc5550a033b2`).
 Numbers and printed pages below belong to that draft, not the published edition.
@@ -345,6 +346,34 @@ two. A correct argument needs the precise equality-test/algebraic-machine restri
 suitable topological obstruction. This observation does not refute the intended undecidability
 result; it prevents using the draft sketch as a complete proof.
 
+## Exercises establishing new theory
+
+The scope includes exercises whose endpoints develop theory, as clarified by Christian
+Reitwiessner; routine practice is not a formalization target. An exercise already implied by
+an existing theorem should be mapped to that theorem rather than reproved. Exercise numbers
+must be pinned to the source chapter, including subparts; placeholders do not supply a precise
+mathematical specification.
+
+The six exercise prompts at the end of Chapter 14 all appear on printed p. 265/PDF p. 281.
+Their current dispositions are:
+
+| Exercise | Endpoint and disposition |
+|---|---|
+| 14 §1 | Finite-field arithmetic versus Boolean circuits up to constant factors. **GF(2) milestone:** [Boolean/Arithmetic.lean](../CslibFrontier/Computability/Circuit/Boolean/Arithmetic.lean) proves same-carrier simulations with size factors three and four, preserving every output. The arbitrary fixed finite-field endpoint remains open; it needs explicit bit representations. |
+| 14 §2 | Circuit depth versus exponential-size straight-line programs. **Source specification needed:** the short prompt does not fix the two directions, costs or parameter relation sufficiently for a formal endpoint. |
+| 14 §3 | The draft only asks “Bauer-Strassen lemma?” **Source specification needed:** select and cite a precise differentiation theorem before implementation; do not silently repair the name and infer a statement. |
+| 14 §4 | Algebraic-machine time to computation-tree depth. **Source issue:** the prompt uses running-time parameter `T` and concludes depth `O(d)` without defining `d`. A corrected endpoint also needs the absent machine/tree model. |
+| 14 §5 | Real BSS computation with arbitrary-precision sign tests decides `P/poly`. **Endpoint not located:** specify the real constants, branch operations and binary-language interface before claiming the circuit-family decoding argument. |
+| 14 §6 | The draft only asks “Shamir's trick?” **Source specification needed:** no exact algorithm, machine model or bound is given in the exercise. |
+
+This is a first exercise inventory, not a complete classification of every chapter's exercises.
+The GF(2) simulations concern values in `Bool`'s Boolean ring, not equality of formal
+polynomials. They use existing gate replacement and four-gate XOR synthesis; no new carrier,
+compiler-runtime claim or general finite-field completion is implied. Their
+[clients](../CslibFrontierTests/BooleanArithmetic.lean) include multiple outputs and zero-cost
+wiring. The remaining theoretical exercises stay under
+[#4711](https://github.com/cslib-community/cslib-frontier/issues/4711).
+
 ## Chapter 16: derandomization and extractors
 
 Snapshot: `b91d5151fd7dc665a5e3efcb466077caf44e690d` on 2026-11-12, with CSLib pin