diff --git a/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean b/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean
index 57e790f58f..e375bd678f 100644
--- a/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean
+++ b/Complexity/Foundations/BooleanAnalysis/BucketWeight.lean
@@ -62,6 +62,7 @@ with `U ∩ J = S`, written `W^{S | J̄} [F]` by O'Donnell, where `J̄` is the c
 noncomputable def bucketWeight (F : (ι → Bool) → ℝ) (J S : Finset ι) : ℝ :=
   ∑ U with U ∩ J = S, fourierCoeff F U ^ 2
 
+/-- Every bucket weight is nonnegative. -/
 theorem bucketWeight_nonneg (F : (ι → Bool) → ℝ) (J S : Finset ι) : 0 ≤ bucketWeight F J S :=
   sum_nonneg fun _ _ => sq_nonneg _
 
diff --git a/Complexity/Foundations/BooleanAnalysis/Fibers.lean b/Complexity/Foundations/BooleanAnalysis/Fibers.lean
index 7c59f9c829..994397a505 100644
--- a/Complexity/Foundations/BooleanAnalysis/Fibers.lean
+++ b/Complexity/Foundations/BooleanAnalysis/Fibers.lean
@@ -58,6 +58,8 @@ light-patterns lemma.
 * `Cslib.BitString.expect_uniformDeficit_coordinateFiber`: Korten's entropy lemma.
 * `Cslib.BitString.coordinateFiber_good_probability`: most fibers have small deficit.
 * `Cslib.BitString.exists_uniformDeficit_fiber_le`: pigeonhole for deficits.
+* `Cslib.BitString.uniformMass_le_rpow`, `Cslib.BitString.uniformDensity_le_rpow`: a deficit
+  bound bounds the uniform probability mass and density pointwise.
 * `Cslib.BitString.coordinateDensity_eq_expect`: the density of a fiber is the probability
   that resampling the coordinates in `s` lands in the set.
 * `Cslib.BitString.projectionAverage_eq_coordinateMarginal`,
@@ -159,7 +161,7 @@ theorem uniformDeficit_le_iff {ι : Type*} [Fintype ι] {X : Finset (ι → Bool
 
 /-- A uniform deficit bound implies the light-patterns lemma's pointwise
 probability-mass hypothesis. -/
-private theorem uniformMass_le_rpow {ι : Type*} [Fintype ι]
+theorem uniformMass_le_rpow {ι : Type*} [Fintype ι]
     {X : Finset (ι → Bool)} (hX : X.Nonempty) {k : ℝ} (hdef : uniformDeficit X ≤ k)
     (x : ι → Bool) : uniformMass X x ≤ (2 : ℝ) ^ (k - Fintype.card ι) := by
   calc
diff --git a/Complexity/Foundations/Combinatorics/Expander/SlotGraph.lean b/Complexity/Foundations/Combinatorics/Expander/SlotGraph.lean
index 7f09d05abe..df1164aeb2 100644
--- a/Complexity/Foundations/Combinatorics/Expander/SlotGraph.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/SlotGraph.lean
@@ -215,7 +215,7 @@ theorem card_slotLabel : Fintype.card SlotLabel = 3 :=
   rfl
 
 /-- The slots of a vertex are reachable from each other along the cycles of `σ`. -/
-theorem reachable_slotGraph_zpow (v w : V) (i : ℤ) :
+private theorem reachable_slotGraph_zpow (v w : V) (i : ℤ) :
     (slotGraph G σ).toSimpleGraph.Reachable (v, w) (v, (σ ^ i) w) := by
   induction i using Int.induction_on with
   | zero => rfl
diff --git a/Complexity/Foundations/Combinatorics/FunctionalGraph/Spectrum.lean b/Complexity/Foundations/Combinatorics/FunctionalGraph/Spectrum.lean
index 6ce4ee6a4a..5f01560ec8 100644
--- a/Complexity/Foundations/Combinatorics/FunctionalGraph/Spectrum.lean
+++ b/Complexity/Foundations/Combinatorics/FunctionalGraph/Spectrum.lean
@@ -89,6 +89,7 @@ section Fintype
 
 variable {α : Type u} [Fintype α] (f : α → α)
 
+/-- The cycle length from any state is at most the cardinality of the state space. -/
 theorem cycleLength_le_card (x : α) : cycleLength f x ≤ Fintype.card α :=
   (Nat.le_add_left _ _).trans (transientDepth_add_cycleLength_le_card f x)
 
diff --git a/Complexity/Foundations/Data/BitString/List.lean b/Complexity/Foundations/Data/BitString/List.lean
index e11cf7e3da..01db52f20a 100644
--- a/Complexity/Foundations/Data/BitString/List.lean
+++ b/Complexity/Foundations/Data/BitString/List.lean
@@ -53,6 +53,7 @@ namespace Cslib.BitString
 /-- View a list as `n` bits, padding missing bits with `false`. -/
 def ofList (n : ℕ) (word : List Bool) : BitString n := fun i => word.getD i.val false
 
+/-- Viewing `List.ofFn bits` as an `n`-bit string recovers `bits`. -/
 @[simp] theorem ofList_ofFn {n : ℕ} (bits : BitString n) :
     ofList n (List.ofFn bits) = bits := by
   funext i
@@ -142,6 +143,7 @@ theorem block_ofList_prefix {count rows width : ℕ} (h : rows ≤ count) (word
 def listRow (width row : ℕ) (word : List Bool) : List Bool :=
   (word.drop (row * width) ++ List.replicate width false).take width
 
+/-- Every extracted row has length `width`. -/
 @[simp] theorem length_listRow (width row : ℕ) (word : List Bool) :
     (listRow width row word).length = width := by
   simp [listRow]
@@ -210,6 +212,7 @@ theorem listRow_eq_ofFn {count : ℕ} (width : ℕ) (row : Fin count) (word : Li
 def listRows (count width : ℕ) (word : List Bool) : List (List Bool) :=
   (List.range count).map (fun row => listRow width row word)
 
+/-- Extracting `count` rows produces a list of length `count`. -/
 @[simp] theorem length_listRows (count width : ℕ) (word : List Bool) :
     (listRows count width word).length = count := by
   simp [listRows]
diff --git a/Complexity/Foundations/Data/Code/Basic.lean b/Complexity/Foundations/Data/Code/Basic.lean
index 49b740d226..5c6acb7064 100644
--- a/Complexity/Foundations/Data/Code/Basic.lean
+++ b/Complexity/Foundations/Data/Code/Basic.lean
@@ -70,6 +70,7 @@ theorem natCast_lt_minDist_iff {r : ℕ} :
   rw [← ENat.natCast_add_one_le_iff, le_minDist_iff]
   simp only [ENat.natCast_add_one_le_iff, Nat.cast_lt]
 
+/-- Distinct codewords are separated by at least the minimum distance of the code. -/
 theorem minDist_le_hammingDist (hx : x ∈ C) (hy : y ∈ C) (hxy : x ≠ y) :
     minDist C ≤ hammingDist x y :=
   le_minDist_iff.1 le_rfl x hx y hy hxy
@@ -85,10 +86,12 @@ theorem minDist_eq_top_iff : minDist C = ⊤ ↔ C.Subsingleton := by
   by_contra hxy
   exact ENat.natCast_ne_top _ (top_le_iff.1 (h x hx y hy hxy))
 
+/-- The empty code has minimum distance `⊤`. -/
 @[simp]
 theorem minDist_empty : minDist (∅ : Set (∀ i, β i)) = ⊤ :=
   minDist_eq_top_iff.2 Set.subsingleton_empty
 
+/-- A singleton code has minimum distance `⊤`. -/
 @[simp]
 theorem minDist_singleton (x : ∀ i, β i) : minDist {x} = ⊤ :=
   minDist_eq_top_iff.2 Set.subsingleton_singleton