diff --git a/Complexity.lean b/Complexity.lean
index fb762678b..46eb90007 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -515,6 +515,7 @@ public import Complexity.Computability.Circuit.Arithmetic.Hessian
 public import Complexity.Computability.Circuit.Arithmetic.Hessian.SourceComplexity
 public import Complexity.Computability.Circuit.Arithmetic.Pairing
 public import Complexity.Computability.Circuit.Arithmetic.Permanent
+public import Complexity.Computability.Circuit.Arithmetic.Permanent.BooleanSum
 public import Complexity.Computability.Circuit.Arithmetic.Permanent.Formula
 public import Complexity.Computability.Circuit.Arithmetic.Power
 public import Complexity.Computability.Circuit.Arithmetic.RelativeRank
@@ -2663,6 +2664,7 @@ public import Complexity.Foundations.Data.Matrix.IntegerBits
 public import Complexity.Foundations.Data.Matrix.PairChunks
 public import Complexity.Foundations.Data.Matrix.Permanent
 public import Complexity.Foundations.Data.Matrix.Permanent.Blocks
+public import Complexity.Foundations.Data.Matrix.Permanent.BooleanSum
 public import Complexity.Foundations.Data.Matrix.Reindex
 public import Complexity.Foundations.Data.Matrix.Ryser
 public import Complexity.Foundations.Data.Matrix.TotallyRegular
diff --git a/Complexity/Computability/Circuit/Arithmetic/Permanent/BooleanSum.lean b/Complexity/Computability/Circuit/Arithmetic/Permanent/BooleanSum.lean
new file mode 100644
index 000000000..5cb4eba48
--- /dev/null
+++ b/Complexity/Computability/Circuit/Arithmetic/Permanent/BooleanSum.lean
@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Arithmetic.Permanent.Formula
+public import Complexity.Computability.Circuit.Arithmetic.VNP
+import Complexity.Foundations.Data.Matrix.Permanent.BooleanSum
+
+/-!
+# Eliminate a selector occurring in one permanent entry
+
+If `K` has a scalar `half` with `2 * half = 1`, a Boolean selector placed in one entry of the
+`d × d` generic permanent can be summed out as a projection of the `(d + 1) × (d + 1)` generic
+permanent. All other entries remain independent variables, in the existing row-major layout.
+The selector is the final variable, following the `d * d` ordinary inputs, so the summation
+uses the existing `booleanSum`.
+
+[Orzel et al., Claim 13, p. 47:10][OrzelSrinivasanTavenasYehudayoff2025] allows a nonzero scalar
+multiplier in projections and therefore states zero extra dimension. The library's
+`IsProjection` permits only substitutions: the factor `2` is represented by a separate scalar
+block, costing one extra matrix dimension. The explicit half hypothesis is essential to this
+construction; it holds over fields of characteristic other than two. Membership in VNP and
+formula simulation have their separately proved, more general ring/semiring scopes.
+
+The selector occurs exactly once in this result. The two-entry gadget, repeated-selector
+elimination, the conversion of VP-based VNP witnesses to formulas, and full VNP-hardness remain
+separate obligations. Only nonuniform projection existence and dimension are certified.
+
+## Main results
+
+* `Cslib.Circuits.Arithmetic.isProjection_booleanSum_entry_permanent`: one extra dimension
+  eliminates a selector in one entry, when `2` has a half.
+
+## References
+
+* [I. Orzel et al.][OrzelSrinivasanTavenasYehudayoff2025], *The Algebraic Cost of a Boolean Sum*,
+  §3.3, Claim 13
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits.Arithmetic
+
+open MvPolynomial
+
+universe u
+
+variable {K : Type u} [CommSemiring K] {d : ℕ}
+
+private def entryAssignment (i j : Fin d) (b : K) : Fin (d * d) → Fin (d * d) ⊕ K :=
+  fun k => if k = finProdFinEquiv (i, j) then .inr b else .inl k
+
+private def selectorAssignment (i j : Fin d) : Fin (d * d) → Fin (d * d + 1) ⊕ K :=
+  fun k => .inl (if k = finProdFinEquiv (i, j) then Fin.natAdd (d * d) 0 else Fin.castAdd 1 k)
+
+private theorem projection_permanent_entry (i j : Fin d) (b : K) :
+    projection (entryAssignment i j b) (genericMatrix K d).permanent =
+      ((genericMatrix K d).updateRow i
+        (Function.update (genericMatrix K d i) j (C b))).permanent := by
+  rw [AlgHom.map_permanent]
+  congr 1
+  apply Matrix.ext
+  intro r c
+  by_cases hr : r = i <;> by_cases hc : c = j <;>
+    simp [genericMatrix, entryAssignment, Matrix.updateRow_apply, hr, hc]
+
+private theorem booleanSum_permanent_entry (i j : Fin d) :
+    booleanSum 1 (projection (selectorAssignment (K := K) i j) (genericMatrix K d).permanent) =
+      projection (entryAssignment i j 0) (genericMatrix K d).permanent +
+        projection (entryAssignment i j 1) (genericMatrix K d).permanent := by
+  rw [booleanSum, ← (Equiv.funUnique (Fin 1) Bool).symm.sum_comp, Fintype.sum_bool, add_comm]
+  simp_rw [projection_projection]
+  congr 1 <;> congr 2 <;> funext k <;>
+    by_cases hk : k = finProdFinEquiv (i, j) <;>
+    simp [selectorAssignment, entryAssignment, booleanAssignment, hk]
+
+/-- A selector occurring in one matrix entry can be summed out using a permanent with one
+extra dimension, under the explicit half-of-two hypothesis. The selector is the last variable;
+the ordinary inputs retain the existing row-major order. -/
+theorem isProjection_booleanSum_entry_permanent (i j : Fin d) (half : K)
+    (hhalf : 2 * half = 1) :
+    IsProjection
+      (booleanSum 1 (projection
+        (fun k : Fin (d * d) => Sum.inl
+          (if k = finProdFinEquiv (i, j) then Fin.natAdd (d * d) 0 else Fin.castAdd 1 k))
+        (genericMatrix K d).permanent))
+      (genericMatrix K (d + 1)).permanent := by
+  change IsProjection
+    (booleanSum 1 (projection (selectorAssignment (K := K) i j) (genericMatrix K d).permanent)) _
+  rw [booleanSum_permanent_entry, projection_permanent_entry, projection_permanent_entry]
+  simp only [map_zero, map_one]
+  have hh : (2 : MvPolynomial (Fin (d * d)) K) * C half = 1 := by
+    rw [← map_ofNat C 2, ← map_mul, hhalf, map_one]
+  rw [Matrix.permanent_updateRow_update_zero_add_one _ i j (C half) hh]
+  have hp : IsProjection
+      (((genericMatrix K d).updateRow i
+        (Function.update (genericMatrix K d i) j (C half))).permanent)
+      (genericMatrix K d).permanent :=
+    ⟨entryAssignment i j half, projection_permanent_entry i j half⟩
+  have hc : IsProjection (2 : MvPolynomial (Fin (d * d)) K) (genericMatrix K 1).permanent := by
+    refine ⟨fun _ => .inr 2, ?_⟩
+    rw [Matrix.permanent_unique]
+    simp only [genericMatrix, Matrix.of_apply, projection_X, Sum.elim_inr]
+    exact map_ofNat C 2
+  simpa only [mul_comm (2 : MvPolynomial (Fin (d * d)) K)] using hp.permanent_mul hc
+
+end Cslib.Circuits.Arithmetic
diff --git a/Complexity/Foundations/Data/Matrix/Permanent/BooleanSum.lean b/Complexity/Foundations/Data/Matrix/Permanent/BooleanSum.lean
new file mode 100644
index 000000000..796fb30e7
--- /dev/null
+++ b/Complexity/Foundations/Data/Matrix/Permanent/BooleanSum.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate (Mathlib, next to `LinearAlgebra/Matrix/Permanent`)
+
+public import Complexity.Foundations.Data.Matrix.Permanent.Blocks
+
+/-!
+# Boolean summation in a single permanent entry
+
+If `2 * half = 1`, adding the permanents obtained by setting one entry to `0` and `1` gives
+twice the permanent with that entry set to `half`. This is the permanent calculation in
+[Orzel et al., Claim 13, p. 47:10][OrzelSrinivasanTavenasYehudayoff2025]. The identity is an
+immediate consequence of row additivity and homogeneity, over any commutative semiring with
+the displayed half-of-two hypothesis.
+
+## Main results
+
+* `Matrix.permanent_updateRow_update_zero_add_one`: eliminate a selector in one entry.
+
+## References
+
+* [I. Orzel et al.][OrzelSrinivasanTavenasYehudayoff2025], *The Algebraic Cost of a Boolean Sum*,
+  §3.3, Claim 13
+-/
+
+@[expose] public section
+
+namespace Matrix
+
+variable {ι R : Type*} [Fintype ι] [DecidableEq ι] [CommSemiring R]
+
+/-- Summing the two Boolean substitutions in one entry equals twice the half-substituted
+permanent. The explicit hypothesis is satisfied when `2` is invertible. -/
+theorem permanent_updateRow_update_zero_add_one (A : Matrix ι ι R) (i j : ι)
+    (half : R) (hhalf : 2 * half = 1) :
+    (A.updateRow i (Function.update (A i) j 0)).permanent +
+        (A.updateRow i (Function.update (A i) j 1)).permanent =
+      2 * (A.updateRow i (Function.update (A i) j half)).permanent := by
+  have hrows : Function.update (A i) j 0 + Function.update (A i) j 1 =
+      (2 : R) • Function.update (A i) j half := by
+    funext k
+    by_cases hk : k = j
+    · subst k
+      simp [hhalf]
+    · simp [Function.update_of_ne hk, two_mul]
+  rw [← permanent_updateRow_add, hrows, permanent_updateRow_smul]
+
+end Matrix
diff --git a/ComplexityTests/PermanentBooleanSum.lean b/ComplexityTests/PermanentBooleanSum.lean
new file mode 100644
index 000000000..849afeb79
--- /dev/null
+++ b/ComplexityTests/PermanentBooleanSum.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Circuit.Arithmetic.Permanent.BooleanSum
+import Complexity.Foundations.Data.Matrix.Permanent
+import Mathlib.Algebra.Field.ZMod
+
+/-!
+# Single-entry selector elimination clients
+
+The selector in `!![b, X₁; X₂, X₃]` is summed over `b = 0, 1`; it gives `2X₁X₂ + X₃`.
+On entries `3,5,7` this is `37`. Both the rational half and the half `2` in `ZMod 3` satisfy
+the construction's hypothesis, while no half exists in `ZMod 2`.
+-/
+
+namespace ComplexityTests.PermanentBooleanSum
+
+open Cslib Cslib.Circuits Cslib.Circuits.Arithmetic MvPolynomial
+
+private noncomputable def selectorPolynomial (K : Type*) [CommSemiring K] :
+    MvPolynomial (Fin (4 + 1)) K :=
+  projection ![Sum.inl 4, .inl 1, .inl 2, .inl 3] (genericMatrix K 2).permanent
+
+private theorem selector_map (K : Type*) :
+    (fun k : Fin 4 => (Sum.inl
+      (if k = finProdFinEquiv ((0 : Fin 2), (0 : Fin 2)) then Fin.natAdd 4 (0 : Fin 1)
+        else Fin.castAdd 1 k) : Fin 5 ⊕ K)) =
+      ![Sum.inl 4, .inl 1, .inl 2, .inl 3] := by
+  funext k
+  fin_cases k <;> rfl
+
+example : IsProjection (booleanSum 1 (selectorPolynomial ℚ)) (genericMatrix ℚ 3).permanent := by
+  have h := isProjection_booleanSum_entry_permanent (K := ℚ) (d := 2) 0 0 (1 / 2)
+    (by norm_num)
+  rw [selector_map] at h
+  exact h
+
+example : IsProjection (booleanSum 1 (selectorPolynomial (ZMod 3)))
+    (genericMatrix (ZMod 3) 3).permanent := by
+  have h := isProjection_booleanSum_entry_permanent (K := ZMod 3) (d := 2) 0 0 2 (by decide)
+  rw [selector_map] at h
+  exact h
+
+private theorem selectorPolynomial_eq (K : Type*) [CommSemiring K] :
+    selectorPolynomial K = X 4 * X 3 + X 1 * X 2 := by
+  unfold selectorPolynomial
+  rw [Matrix.permanent_succ_row_zero, Fin.sum_univ_two, Matrix.permanent_succ_row_zero,
+    Matrix.permanent_succ_row_zero, Fin.sum_univ_one, Fin.sum_univ_one]
+  simp [Matrix.permanent, genericMatrix, finProdFinEquiv]
+
+private theorem booleanSum_selectorPolynomial : booleanSum 1 (selectorPolynomial ℚ) =
+    2 * X 1 * X 2 + X 3 := by
+  rw [selectorPolynomial_eq, booleanSum,
+    ← (Equiv.funUnique (Fin 1) Bool).symm.sum_comp, Fintype.sum_bool]
+  have h2 (h : (2 : Fin 5) ≠ Fin.last 4) : Fin.castPred (2 : Fin 5) h = (2 : Fin 4) := rfl
+  have h3 (h : (3 : Fin 5) ≠ Fin.last 4) : Fin.castPred (3 : Fin 5) h = (3 : Fin 4) := rfl
+  norm_num [booleanAssignment, Fin.append, Fin.addCases, h2, h3]
+  ring
+
+example : aeval (![99, 3, 5, 7] : Fin 4 → ℚ)
+    (booleanSum 1 (selectorPolynomial ℚ)) = 37 := by
+  rw [booleanSum_selectorPolynomial]
+  norm_num
+
+example : booleanSum 1 (projection (fun _ : Fin 1 => (Sum.inl (1 : Fin 2) : Fin 2 ⊕ ℚ))
+    (genericMatrix ℚ 1).permanent) = 1 := by
+  rw [Matrix.permanent_unique, booleanSum,
+    ← (Equiv.funUnique (Fin 1) Bool).symm.sum_comp, Fintype.sum_bool]
+  norm_num [genericMatrix, booleanAssignment, Fin.append, Fin.addCases]
+
+example : ¬ ∃ half : ZMod 2, 2 * half = 1 := by
+  rintro ⟨half, hhalf⟩
+  have htwo : (2 : ZMod 2) = 0 := by decide
+  rw [htwo, zero_mul] at hhalf
+  exact zero_ne_one hhalf
+
+end ComplexityTests.PermanentBooleanSum
diff --git a/ROADMAP.md b/ROADMAP.md
index 8659366b6..bc0f2a436 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -808,8 +808,9 @@ not planned, not as proved.
 
 - The full VNP-completeness reduction for the permanent ([#321]). Arithmetic formulas now
   project to the permanent with dimension `Formula.size + 1` over every commutative semiring;
-  the conversion from VP witnesses to formulas and elimination of Boolean sums needed for
-  VNP-hardness remain open.
+  a selector occurring in one permanent entry can be eliminated with one extra dimension when
+  `2` is invertible. The conversion from VP witnesses to formulas, the two-entry gadget and
+  general Boolean-sum elimination needed for VNP-hardness remain open.
 - General auxiliary-input zero knowledge ([#324]); see the GMW theorem above.
 - Williams's square-root-space simulation ([#361]) and implicit Tree Evaluation ([#367]), now the
   frontier track [#888].