SamuelSchlesinger · Oct 24, 2026 · Oct 23, 2026
diff --git a/Complexity.lean b/Complexity.lean
@@ -1597,6 +1597,7 @@ public import Complexity.Foundations.Data.BitString.Multiplication
 public import Complexity.Foundations.Data.BitString.PackedCount
 public import Complexity.Foundations.Data.BitString.Packing
 public import Complexity.Foundations.Data.BitString.Parity
+public import Complexity.Foundations.Data.BitString.Parity.Weight
 public import Complexity.Foundations.Data.BitString.PartialAssignment
 public import Complexity.Foundations.Data.BitString.Point
 public import Complexity.Foundations.Data.BitString.Projection

diff --git a/Complexity/Computability/Circuit/Boolean/FanInTwo.lean b/Complexity/Computability/Circuit/Boolean/FanInTwo.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Circuit.Boolean.DepthClasses
 public import Complexity.Computability.Circuit.Boolean.Formula
 public import Complexity.Computability.Circuit.MapLines
 public import Complexity.Computability.Circuit.SimulationDepth
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Computability.Circuit.Program
 import Complexity.Computability.Circuit.Simulation
 import Complexity.Foundations.Data.Nat.PolynomialBound.Log

diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Circuit.Boolean.FirstOrder
 public import Mathlib.Order.Filter.AtTopBot.Defs
 public import Mathlib.SetTheory.Cardinal.Finite
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Computability.Circuit.Boolean.Hastad
 import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
 import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential

diff --git a/Complexity/Computability/Circuit/Boolean/HardCore.lean b/Complexity/Computability/Circuit/Boolean/HardCore.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Circuit.Boolean.AtLeast
 public import Complexity.Computability.Circuit.Boolean.Synthesis
 public import Mathlib.Basic.Real.Basic
+import Complexity.Foundations.Data.BitString.Basic
 import Complexity.Crypto.Computational.Pseudoentropy.Boosting.Potential
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.Order.BigOperators.Group.Finset

diff --git a/Complexity/Computability/Circuit/Boolean/HardnessAmplification/WorstCase.lean b/Complexity/Computability/Circuit/Boolean/HardnessAmplification/WorstCase.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Circuit.Boolean.HardnessAmplification.Sta
 public import Complexity.Foundations.BooleanAnalysis.Hadamard
 public import Complexity.Foundations.Data.Code.Concatenation
 public import Complexity.Foundations.Data.Code.LowDegreeExtension
+import Complexity.Foundations.Data.BitString.Basic
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.Positivity

diff --git a/Complexity/Computability/Circuit/Boolean/Majority.lean b/Complexity/Computability/Circuit/Boolean/Majority.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Circuit.Boolean.AC0
 public import Complexity.Foundations.Data.BitString.Weight
+import Complexity.Foundations.Data.BitString.Parity.Weight
 import Complexity.Foundations.Data.Fin.Append
 import Mathlib.Data.Fintype.Fin
 

diff --git a/Complexity/Computability/Circuit/Boolean/Multiplicity.lean b/Complexity/Computability/Circuit/Boolean/Multiplicity.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Circuit.Boolean.FanInTwo
+import Mathlib.Algebra.BigOperators.Fin
 
 /-!
 # Symmetric gates reading their wires with multiplicities

diff --git a/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean b/Complexity/Computability/Circuit/Boolean/Threshold/Parity.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Circuit.Boolean.ConstDepth
 public import Complexity.Computability.Circuit.Boolean.Threshold
 public import Complexity.Computability.Circuit.Simulation
+public import Complexity.Foundations.Data.BitString.Parity.Weight
 import Mathlib.Algebra.BigOperators.Fin
 
 /-!

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Init
 public import Complexity.Computability.Circuit.Boolean.WeightedThreshold.CapacityCircuit
+import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Data.Int.Interval
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Complexity.Computability.Circuit.Boolean.WeightedThreshold.CapacityCircuit
 public import Complexity.Foundations.BooleanAnalysis.Hadamard
+import Mathlib.Algebra.BigOperators.Fin
 
 /-!
 # Pending-bias state simulation and input-summary lower bounds for threshold circuits

diff --git a/Complexity/Computability/Circuit/Boolean/XorLemma.lean b/Complexity/Computability/Circuit/Boolean/XorLemma.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Circuit.Boolean.HardCore
 public import Complexity.Foundations.Data.BitString.Block
 public import Complexity.Foundations.Data.BitString.Parity
+import Complexity.Foundations.Data.BitString.Basic
 import Complexity.Computability.Circuit.Boolean.Substitution
 import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.Finset

diff --git a/Complexity/Computability/Complexity/AffineDisperser/Program.lean b/Complexity/Computability/Complexity/AffineDisperser/Program.lean
@@ -11,6 +11,7 @@ public import Complexity.Init
 public import Complexity.Computability.Complexity.AffineDisperser.BinaryPolynomial
 public import Complexity.Computability.Complexity.AffineDisperser.Coordinates
 public import Complexity.Foundations.Combinatorics.AffineDisperser.Explicit
+import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/PCP/AssignmentTester.lean b/Complexity/Computability/PCP/AssignmentTester.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.PCP.LocalTest
 public import Complexity.Foundations.BooleanAnalysis.HadamardTester
 public import Mathlib.Data.Fin.VecNotation
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Foundations.Data.Finset.Expect
 import Complexity.Foundations.Data.Hamming
 import Mathlib.Algebra.Order.BigOperators.Expect

diff --git a/Complexity/Crypto/Computational/GoldreichLevin/Nonuniform.lean b/Complexity/Crypto/Computational/GoldreichLevin/Nonuniform.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Crypto.Computational.GoldreichLevin.Decoding
+import Complexity.Foundations.Data.BitString.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Integrals
 
 /-!

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Foundations.Data.List.Basic
 
 /-!

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Foundations.Data.List.Basic
 import Complexity.Foundations.Data.Nat.Bits
 

diff --git a/Complexity/Foundations/BooleanAnalysis/Convolution.lean b/Complexity/Foundations/BooleanAnalysis/Convolution.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Foundations.BooleanAnalysis.Fourier
+import Complexity.Foundations.Data.BitString.Basic
 import Complexity.Foundations.Data.Finset.Expect
 import Mathlib.Tactic.Ring
 

diff --git a/Complexity/Foundations/BooleanAnalysis/PolynomialCorrelation.lean b/Complexity/Foundations/BooleanAnalysis/PolynomialCorrelation.lean
@@ -14,6 +14,7 @@ public import Complexity.Foundations.Data.BitString.Weight
 public import Mathlib.Analysis.Real.Sqrt
 public import Mathlib.Data.ZMod.Defs
 public import Mathlib.Logic.Equiv.Fin.Basic
+import Complexity.Foundations.Data.BitString.Basic
 import Complexity.Foundations.Combinatorics.CentralBinomial
 import Mathlib.Algebra.CharP.Two
 import Mathlib.Algebra.Field.ZMod

diff --git a/Complexity/Foundations/Data/BitString/Hamming.lean b/Complexity/Foundations/Data/BitString/Hamming.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Foundations.Data.BitString.Weight
+public import Complexity.Foundations.Data.BitString.Parity
 
 /-!
 # The Hamming geometry of the Boolean cube

diff --git a/Complexity/Foundations/Data/BitString/List/Operations.lean b/Complexity/Foundations/Data/BitString/List/Operations.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Foundations.Data.BitString.List
 public import Complexity.Foundations.Data.BitString.Weight
 public import Mathlib.Data.Matrix.Mul
+import Mathlib.Algebra.BigOperators.Fin
 
 /-!
 # Algebraic operations on lists of bits

diff --git a/Complexity/Foundations/Data/BitString/Parity.lean b/Complexity/Foundations/Data/BitString/Parity.lean
@@ -7,7 +7,8 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Foundations.Data.BitString.Basic
+public import Cslib.Foundations.Data.BitString
+public import Mathlib.Algebra.Ring.BooleanRing
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 public import Mathlib.Algebra.Group.Hom.Defs
 public import Mathlib.Data.Finset.Card
@@ -19,7 +20,6 @@ public import Mathlib.Data.Fintype.Pi
 public import Mathlib.Logic.Function.Const
 public import Mathlib.Logic.Function.DependsOn
 import Mathlib.Algebra.BigOperators.Ring.Finset
-import Mathlib.Algebra.Ring.BooleanRing
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.GroupTheory.Index
 
@@ -34,7 +34,7 @@ In the Boolean ring `Bool`, where `a + b = (a ^^ b)`, the parity on `s` is the s
 `s` (`parityOn_eq_sum`), so it splits over disjoint unions (`parityOn_union`), the parity on a
 symmetric difference is the exclusive or of the parities (`parityOn_symmDiff`), and it is additive
 for the coordinatewise sum of bit strings (`parityOn_add`, bundled as `parityOnAddMonoidHom`). Bit
-strings are added with `+`, under which each is its own negative (`BitString.add_self`), and
+strings are added with `+`, under which each is its own negative (`BooleanRing.add_self`), and
 single bits with `^^`. Flipping one of the bits negates the parity (`parityOn_update_not`), so
 the parity of a nonempty set of bits is not constant and depends on each of them; being additive,
 it then takes each value on exactly half of the inputs (`card_filter_parityOn_eq`).

diff --git a/Complexity/Foundations/Data/BitString/Parity/Weight.lean b/Complexity/Foundations/Data/BitString/Parity/Weight.lean
@@ -0,0 +1,40 @@
+/-
+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.Foundations.Data.BitString.Parity
+public import Complexity.Foundations.Data.BitString.Weight
+
+/-!
+# Parity and Hamming weight
+
+The parity of a bit string is the parity of its Hamming weight (`Cslib.parity_eq_decide_weight`),
+so parity is a symmetric Boolean function (`Cslib.isSymmetric_parity`). This bridge is kept apart
+from both `BitString.Parity` and `BitString.Weight`, so that neither of them imports the other.
+
+## Main results
+
+* `Cslib.parity_eq_decide_weight`: parity is the parity of the weight.
+* `Cslib.isSymmetric_parity`: parity is symmetric.
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+/-- Parity is the parity of the weight. -/
+theorem parity_eq_decide_weight {n : ℕ} (x : BitString n) :
+    parity n x = decide (BitString.weight x % 2 = 1) :=
+  rfl
+
+/-- Parity is symmetric. -/
+theorem isSymmetric_parity {n : ℕ} : (parity n).IsSymmetric := fun x y h => by
+  simp only [BitString.weight] at h
+  simp only [parity, parityOn, h]
+
+end Cslib
diff --git a/Complexity/Foundations/Data/BitString/Weight.lean b/Complexity/Foundations/Data/BitString/Weight.lean
@@ -7,7 +7,8 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Foundations.Data.BitString.Parity
+public import Cslib.Foundations.Data.BitString
+public import Mathlib.Algebra.Ring.BooleanRing
 public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 public import Mathlib.Data.Fintype.Sum
 public import Mathlib.Data.Nat.Choose.Basic
@@ -48,8 +49,7 @@ function is *symmetric* when it depends only on the weight of its input
 * `Cslib.strictMajority_not`: strict majority of the negated bits is the negation of majority.
 * `Cslib.BitString.strictMajorityOn`: strict majority on a finite set of voting indices.
 * `Cslib.le_card_ne_of_strictMajority_ne`: a wrong majority requires at least half wrong votes.
-* `Cslib.isSymmetric_threshold`, `Cslib.isSymmetric_parity`: threshold functions and parity are
-  symmetric.
+* `Cslib.isSymmetric_threshold`: threshold functions are symmetric.
 
 ## References
 
@@ -354,13 +354,4 @@ theorem isSymmetric_majority : (majority n).IsSymmetric :=
 theorem isSymmetric_strictMajority : (strictMajority n).IsSymmetric :=
   isSymmetric_threshold _
 
-/-- Parity is the parity of the weight. -/
-theorem parity_eq_decide_weight (x : BitString n) : parity n x = decide (weight x % 2 = 1) :=
-  rfl
-
-/-- Parity is symmetric. -/
-theorem isSymmetric_parity : (parity n).IsSymmetric := fun x y h => by
-  simp only [weight] at h
-  simp only [parity, parityOn, h]
-
 end Cslib
diff --git a/Complexity/Languages/Probabilistic/Repeat.lean b/Complexity/Languages/Probabilistic/Repeat.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Languages.Probabilistic.Basic
 public import Complexity.Probability.BitString.List
 public import Complexity.Probability.Product
+import Mathlib.Algebra.BigOperators.Fin
 
 /-!
 # Bounded repetition of probabilistic programs

diff --git a/Complexity/Logics/Propositional/CNF/Parity.lean b/Complexity/Logics/Propositional/CNF/Parity.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Foundations.Data.BitString.Parity
 public import Complexity.Logics.Propositional.CNF
+public import Mathlib.Data.Finset.Powerset
 
 /-!
 # Parity constraints in conjunctive normal form

diff --git a/ComplexityTests/HardnessAmplification.lean b/ComplexityTests/HardnessAmplification.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
+import Complexity.Foundations.Data.BitString.Basic
 import Complexity.Computability.Circuit.Boolean.XorLemma
 
 /-! Impagliazzo's hard-core lemma and Yao's XOR lemma: a concrete hard-core measure, the

diff --git a/ComplexityTests/HastadSharp.lean b/ComplexityTests/HastadSharp.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
+import Complexity.Foundations.Data.BitString.Parity.Weight
 import Complexity.Computability.Circuit.Boolean.Hastad.Sharp
 import Complexity.Computability.Circuit.Boolean.FirstOrder.Parity
 import Complexity.Computability.Circuit.Boolean.ShallowSymmetric

diff --git a/ComplexityTests/QueryComplexity/Randomized.lean b/ComplexityTests/QueryComplexity/Randomized.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Computability.QueryComplexity.ApproximateDegree.Or
 import Complexity.Computability.QueryComplexity.Randomized.Nisan
 import Complexity.Computability.QueryComplexity.Yao

diff --git a/ComplexityTests/QueryComplexity/Sensitivity.lean b/ComplexityTests/QueryComplexity/Sensitivity.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
+import Complexity.Foundations.Data.BitString.Parity.Weight
 import Complexity.Computability.DecisionTree.Symmetric
 import Complexity.Computability.QueryComplexity.Monotone
 import Complexity.Computability.QueryComplexity.SensitivityBounds

diff --git a/ComplexityTests/ThresholdCapacityCircuit.lean b/ComplexityTests/ThresholdCapacityCircuit.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Computability.Circuit.Boolean.WeightedThreshold.CapacityCircuit
 import Mathlib.Data.Fintype.Powerset
 import Mathlib.Tactic.FinCases

diff --git a/ComplexityTests/ThresholdInnerProduct.lean b/ComplexityTests/ThresholdInnerProduct.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
+import Mathlib.Algebra.BigOperators.Fin
 import Complexity.Foundations.BooleanAnalysis.HadamardRectangles
 import Complexity.Computability.DecisionTree.InnerProduct
 import Mathlib.Data.Fintype.Powerset