refactor(classes): make proof helpers private across the classes area

Complexity/Computability/Communication/Discrepancy.lean

@@ -142,7 +142,7 @@ theorem abs_sum_mul_signVal_le [Fintype X] [Fintype Y] (p : Protocol X Y Bool) (
 
 /-- The correlation under `ν` of `f` with the output of a protocol is `1 - 2 ε`, where `ε` is the
 probability that the protocol errs on inputs drawn from `ν`. -/
-theorem sum_mul_signVal_eq [Fintype X] [Fintype Y] (p : Protocol X Y Bool) (ν : PMF (X × Y))
+private theorem sum_mul_signVal_eq [Fintype X] [Fintype Y] (p : Protocol X Y Bool) (ν : PMF (X × Y))
     (f : X → Y → Bool) :
     ∑ x, ∑ y, (ν (x, y)).toReal * signVal (f x y) * signVal (p.run x y) =
       1 - 2 * p.distributionalError ν (fun x y b => f x y = b) := by

Complexity/Computability/Communication/Functions.lean

@@ -206,7 +206,7 @@ theorem two_mul_card_dotProduct_eq_true_add [DecidableEq ι] (x : ι → Bool) :
 
 /-- The inner product is `true` on `2 ^ (k - 1) (2 ^ k - 1)` pairs of `k`-bit strings, in the form
 `2 c + 2 ^ k = 2 ^ k 2 ^ k`. -/
-theorem two_mul_card_dotProduct_eq_true_add_two_pow [DecidableEq ι] :
+private theorem two_mul_card_dotProduct_eq_true_add_two_pow [DecidableEq ι] :
     2 * #{q : (ι → Bool) × (ι → Bool) | q.1 ⬝ᵥ q.2 = true} + 2 ^ Fintype.card ι =
       2 ^ Fintype.card ι * 2 ^ Fintype.card ι := by
   have hrow : #{q : (ι → Bool) × (ι → Bool) | q.1 ⬝ᵥ q.2 = true} =

Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean

@@ -71,7 +71,7 @@ theorem polyOfBits_nil : polyOfBits [] = 0 := rfl
 theorem polyOfBits_cons (b : Bool) (l : List Bool) :
     polyOfBits (b :: l) = C (bitEquiv.symm b) + X * polyOfBits l := rfl
 
-theorem polyOfBits_append (l l' : List Bool) :
+private theorem polyOfBits_append (l l' : List Bool) :
     polyOfBits (l ++ l') = polyOfBits l + X ^ l.length * polyOfBits l' := by
   induction l with
   | nil => simp
@@ -86,11 +86,11 @@ theorem polyOfBits_replicate_false (k : ℕ) : polyOfBits (List.replicate k fals
   | succ k ih => simp [List.replicate_succ, ih, bitEquiv_symm_false]
 
 /-- The coefficient list of the monomial `X ^ k`. -/
-theorem polyOfBits_replicate_append_true (k : ℕ) :
+private theorem polyOfBits_replicate_append_true (k : ℕ) :
     polyOfBits (List.replicate k false ++ [true]) = X ^ k := by
   simp [polyOfBits_append, bitEquiv_symm_true]
 
-theorem polyOfBits_zipWith_xor {l l' : List Bool} (h : l.length = l'.length) :
+private theorem polyOfBits_zipWith_xor {l l' : List Bool} (h : l.length = l'.length) :
     polyOfBits (l.zipWith xor l') = polyOfBits l + polyOfBits l' := by
   induction l generalizing l' with
   | nil => cases l' <;> simp_all
@@ -121,7 +121,7 @@ theorem polyOfBits_eq_zero_iff {l : List Bool} : polyOfBits l = 0 ↔ ∀ b ∈
       rw [h, bitEquiv_symm_false]
       simp
 
-theorem degree_polyOfBits_lt (l : List Bool) : (polyOfBits l).degree < l.length := by
+private theorem degree_polyOfBits_lt (l : List Bool) : (polyOfBits l).degree < l.length := by
   induction l with
   | nil => simp
   | cons b l ih =>
@@ -138,7 +138,7 @@ theorem degree_polyOfBits_lt (l : List Bool) : (polyOfBits l).degree < l.length
         omega
 
 /-- Dropping a top coefficient that is zero does not change the polynomial. -/
-theorem polyOfBits_take_of_getD {l : List Bool} {m : ℕ} (hl : l.length = m + 1)
+private theorem polyOfBits_take_of_getD {l : List Bool} {m : ℕ} (hl : l.length = m + 1)
     (htop : l.getD m false = false) : polyOfBits (l.take m) = polyOfBits l := by
   conv_rhs => rw [← List.take_append_drop m l]
   have hdrop : l.drop m = [false] := by
@@ -148,7 +148,7 @@ theorem polyOfBits_take_of_getD {l : List Bool} {m : ℕ} (hl : l.length = m + 1
   rw [hdrop, polyOfBits_append]
   simp [bitEquiv_symm_false]
 
-theorem aeval_polyOfBits {A : Type*} [CommSemiring A] [Algebra (ZMod 2) A] (α : A)
+private theorem aeval_polyOfBits {A : Type*} [CommSemiring A] [Algebra (ZMod 2) A] (α : A)
     (l : List Bool) :
     aeval α (polyOfBits l) =
       ∑ d ∈ Finset.range l.length, bitEquiv.symm (l.getD d false) • α ^ d := by
@@ -204,12 +204,12 @@ def mulXMod (g r : List Bool) : List Bool :=
   (if (false :: r).getD (g.length - 1) false then (false :: r).zipWith xor g
     else false :: r).take (g.length - 1)
 
-theorem length_mulXMod (l r : List Bool) (h : r.length = l.length) :
+private theorem length_mulXMod (l r : List Bool) (h : r.length = l.length) :
     (mulXMod (l ++ [true]) r).length = l.length := by
   unfold mulXMod
   split_ifs <;> simp [h]
 
-theorem mk_polyOfBits_mulXMod (l r : List Bool) (h : r.length = l.length) :
+private theorem mk_polyOfBits_mulXMod (l r : List Bool) (h : r.length = l.length) :
     AdjoinRoot.mk (polyOfBits (l ++ [true])) (polyOfBits (mulXMod (l ++ [true]) r)) =
       AdjoinRoot.mk (polyOfBits (l ++ [true])) (X * polyOfBits r) := by
   have hlen : (l ++ [true]).length - 1 = l.length := by simp
@@ -276,7 +276,7 @@ private theorem modStep_foldl (l f p a : List Bool) (hp : p.length = l.length)
         simp only [map_add, map_mul, map_zero]
         ring
 
-theorem length_modBits (l f : List Bool) : (modBits (l ++ [true]) f).length = l.length := by
+private theorem length_modBits (l f : List Bool) : (modBits (l ++ [true]) f).length = l.length := by
   have hlen : (l ++ [true]).length - 1 = l.length := by simp
   unfold modBits
   rw [hlen]
@@ -303,7 +303,7 @@ theorem mk_polyOfBits_modBits (l f : List Bool) :
   simp
 
 
-theorem polyOfBits_append_true_ne_zero (l : List Bool) : polyOfBits (l ++ [true]) ≠ 0 := by
+private theorem polyOfBits_append_true_ne_zero (l : List Bool) : polyOfBits (l ++ [true]) ≠ 0 := by
   rw [Ne, polyOfBits_eq_zero_iff]
   intro h
   exact Bool.true_eq_false.mp (h true (by simp))
@@ -323,12 +323,12 @@ theorem modBits_all_false_iff (l f : List Bool) :
 private theorem monic_of_ne_zero {q : (ZMod 2)[X]} (hq : q ≠ 0) : q.Monic :=
   (by decide : ∀ c : ZMod 2, c ≠ 0 → c = 1) _ (leadingCoeff_ne_zero.2 hq)
 
-theorem natDegree_polyOfCode_eq_log (m : ℕ) : (polyOfCode m).natDegree = Nat.log 2 m := by
+private theorem natDegree_polyOfCode_eq_log (m : ℕ) : (polyOfCode m).natDegree = Nat.log 2 m := by
   rcases eq_or_ne m 0 with rfl | hm
   · simp
   · exact natDegree_polyOfCode hm
 
-theorem polyOfCode_one : polyOfCode 1 = 1 := by
+private theorem polyOfCode_one : polyOfCode 1 = 1 := by
   rw [← polyOfBits_bits, Nat.one_bits]
   simp [bitEquiv_symm_true]
 
@@ -436,7 +436,7 @@ polynomial with coefficient list `g`. -/
 def powerTable (g : List Bool) : List (List Bool) :=
   (List.range (2 * (g.length - 1))).map fun e => modBits g (List.replicate e false ++ [true])
 
-theorem length_powerTable (g : List Bool) : (powerTable g).length = 2 * (g.length - 1) := by
+private theorem length_powerTable (g : List Bool) : (powerTable g).length = 2 * (g.length - 1) := by
   simp [powerTable]
 
 /-- At a root `α` of the polynomial with coefficient list `l ++ [true]`, the power `α ^ e`,

Complexity/Computability/Complexity/AffineDisperser/Coordinates.lean

@@ -76,7 +76,7 @@ theorem repr_fieldOfBits (B : Basis (Fin n) (ZMod 2) F) (a : List Bool) (u : Fin
 theorem fieldOfBits_nil (B : Basis (Fin n) (ZMod 2) F) : fieldOfBits B [] = 0 := by
   simp [fieldOfBits]
 
-theorem bitEquiv_symm_foldl_xor (l : List Bool) :
+private theorem bitEquiv_symm_foldl_xor (l : List Bool) :
     bitEquiv.symm (l.foldl xor false) = (l.map bitEquiv.symm).sum := by
   rw [← map_list_sum]
   congr 1
@@ -287,7 +287,7 @@ private theorem getD_take_drop (x : List Bool) {n u : ℕ} (hu : u < n) (i : ℕ
   rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_take_of_lt hu,
     List.getElem?_drop]
 
-theorem readField_blockPos (B : Basis (Fin n) (ZMod 2) F) {r N : ℕ} (h : r * n ≤ N)
+private theorem readField_blockPos (B : Basis (Fin n) (ZMod 2) F) {r N : ℕ} (h : r * n ≤ N)
     (x : List Bool) (i : Fin r) :
     readField B (blockPos h) (ofList N x) i = fieldOfBits B ((x.drop (n * i)).take n) := by
   refine Finset.sum_congr rfl fun u _ => ?_

Complexity/Computability/Complexity/AffineDisperser/Program.lean

@@ -84,7 +84,7 @@ def monomialTable (ms : List ℕ) (R : List (List (List Bool))) : List (List (Li
     (List.range ms.prod).map fun v => monomialBit ms R u w v
 
 /-- The mixed-radix digits are the components of `finPiFinEquiv.symm`. -/
-theorem mixedDigit_eq (ms : List ℕ) (u : Fin (∏ i, ms.get i)) (i : Fin ms.length) :
+private theorem mixedDigit_eq (ms : List ℕ) (u : Fin (∏ i, ms.get i)) (i : Fin ms.length) :
     mixedDigit ms u i = (finPiFinEquiv.symm u i : ℕ) := by
   have hprod : ∏ j : Fin i, ms.get (Fin.castLE i.is_lt.le j) = (ms.take i).prod := by
     rw [← List.prod_ofFn]
@@ -109,7 +109,7 @@ private theorem bitEquiv_symm_all (k : ℕ) (p : ℕ → Bool) :
     rw [Bool.not_eq_true] at hpi
     simp [hpi]
 
-theorem tableEntry_monomialTable {ms : List ℕ} {R : List (List (List Bool))} {u w : ℕ}
+private theorem tableEntry_monomialTable {ms : List ℕ} {R : List (List (List Bool))} {u w : ℕ}
     (hu : u < ms.prod) (hw : w < ms.prod) :
     tableEntry (monomialTable ms R) u w = (List.range ms.prod).map (monomialBit ms R u w) := by
   simp [tableEntry, monomialTable, List.getD_eq_getElem?_getD, hu, hw]
@@ -190,13 +190,14 @@ theorem aeval_binaryRoot_degreePrime (N : ℕ) (j : Fin (degreePrimes N).length)
   exact minpoly.aeval _ _
 
 /-- The basis of the explicit disperser is the monomial basis in the roots `binaryRoot`. -/
-theorem explicitBasis_eq_rootBasis (N : ℕ) :
+private theorem explicitBasis_eq_rootBasis (N : ℕ) :
     explicitBasis N = rootBasis N (fun j => binaryRoot (degreePrime N j) (fieldDegree N))
       (aeval_binaryRoot_degreePrime N) :=
   rfl
 
 /-- The explicit table is the multiplication table of the monomial basis in any roots. -/
-theorem isMulTable_explicitTable (N : ℕ) (α : (j : Fin (degreePrimes N).length) → ExplicitField N)
+private theorem isMulTable_explicitTable (N : ℕ)
+    (α : (j : Fin (degreePrimes N).length) → ExplicitField N)
     (hα : ∀ j, aeval (α j) (leastIrreducible (degreePrime N j)) = 0) :
     IsMulTable ((rootBasis N α hα).reindex finPiFinEquiv) (explicitTable N) := by
   refine isMulTable_monomialTable _ _ _ _ _ fun i e he => ?_
@@ -228,7 +229,7 @@ theorem isMulTable_explicitTable (N : ℕ) (α : (j : Fin (degreePrimes N).lengt
 
 omit [FiniteDimensional (ZMod 2) F] in
 /-- Reindexing the basis and the reading positions together does not change `traceSymBits`. -/
-theorem traceSymBits_reindex {ι ι' : Type*} [Fintype ι] [Fintype ι'] {r t N : ℕ} (μ : F)
+private theorem traceSymBits_reindex {ι ι' : Type*} [Fintype ι] [Fintype ι'] {r t N : ℕ} (μ : F)
     (b : Basis ι (ZMod 2) F) (e : ι ≃ ι') (pos : Fin r × ι' → Fin N) (x : BitString N) :
     traceSymBits μ r t (b.reindex e) pos x =
       traceSymBits μ r t b (fun q => pos (q.1, e q.2)) x := by
@@ -241,7 +242,7 @@ theorem traceSymBits_reindex {ι ι' : Type*} [Fintype ι] [Fintype ι'] {r t N
 /-- The coordinate computation with the explicit table is `traceSymBits` in the monomial basis in
 any roots `α` of the least-code irreducible polynomials, read on the first `N` bits of `x` (missing
 bits are zero). -/
-theorem traceSymCoords_explicitTable_eq_traceSymBits (N : ℕ)
+private theorem traceSymCoords_explicitTable_eq_traceSymBits (N : ℕ)
     (α : (j : Fin (degreePrimes N).length) → ExplicitField N)
     (hα : ∀ j, aeval (α j) (leastIrreducible (degreePrime N j)) = 0) (x : List Bool) :
     traceSymCoords (explicitTable N) (numBlocks N) (symDegree N) x =

Complexity/Computability/Complexity/Classes/Alternation/Savitch.lean

@@ -115,16 +115,16 @@ def midpointMoves (w : ℕ) (z : List Bool) : List Bool :=
   (List.range w).map fun j => z.getD (2 * j) false
 
 /-- A midpoint has width `w`. -/
-theorem length_midpointMoves (w : ℕ) (z : List Bool) : (midpointMoves w z).length = w := by
+private theorem length_midpointMoves (w : ℕ) (z : List Bool) : (midpointMoves w z).length = w := by
   simp [midpointMoves]
 
 /-- The first round of a level writes the first bit of the midpoint. -/
-theorem midpointMoves_cons_cons (w : ℕ) (x y : Bool) (z : List Bool) :
+private theorem midpointMoves_cons_cons (w : ℕ) (x y : Bool) (z : List Bool) :
     midpointMoves (w + 1) (x :: y :: z) = x :: midpointMoves w z := by
   simp [midpointMoves, List.range_succ_eq_map, Nat.mul_succ]
 
 /-- The midpoint only reads the first `2 * w` moves. -/
-theorem midpointMoves_take {w n : ℕ} (hn : 2 * w ≤ n) (z : List Bool) :
+private theorem midpointMoves_take {w n : ℕ} (hn : 2 * w ≤ n) (z : List Bool) :
     midpointMoves w (z.take n) = midpointMoves w z := by
   refine List.map_congr_left fun j hj => ?_
   rw [List.mem_range] at hj
@@ -147,7 +147,7 @@ def midpointGame (edge : List Bool → List Bool → Bool) (w : ℕ) :
 variable {edge : List Bool → List Bool → Bool} {w : ℕ}
 
 /-- The game at level `i` reads only its first `2 * ((w + 1) * i)` moves. -/
-theorem midpointGame_take (i : ℕ) (u v z : List Bool) :
+private theorem midpointGame_take (i : ℕ) (u v z : List Bool) :
     midpointGame edge w i u v (z.take (2 * ((w + 1) * i))) = midpointGame edge w i u v z := by
   induction i generalizing u v z with
   | zero => rfl
@@ -167,7 +167,7 @@ theorem midpointGame_take (i : ℕ) (u v z : List Bool) :
     simp only [midpointGame, hget, hmid, hdrop, ih]
 
 /-- The existential player chooses a midpoint in `w` rounds. -/
-theorem alternation_midpointMoves (j : ℕ) {ns : List ℕ} :
+private theorem alternation_midpointMoves (j : ℕ) {ns : List ℕ} :
     ∀ R : List Bool → List Bool → Prop,
       Alternation true (List.replicate (2 * j) 1 ++ ns)
         (fun z => R (midpointMoves j z) (z.drop (2 * j))) ↔
@@ -191,7 +191,7 @@ theorem alternation_midpointMoves (j : ℕ) {ns : List ℕ} :
       · exact ⟨x, fun _ => ⟨m, by simpa using hm, h⟩⟩
 
 /-- The universal player chooses a half in one round. -/
-theorem alternation_half {ns : List ℕ} (S : Bool → List Bool → Prop) :
+private theorem alternation_half {ns : List ℕ} (S : Bool → List Bool → Prop) :
     Alternation true (1 :: 1 :: ns) (fun z => S (z.getD 1 false) (z.drop 2)) ↔
       ∀ d, Alternation true ns (S d) := by
   rw [alternation_true_one_cons]

Complexity/Computability/Complexity/Classes/Alternation/TQBF.lean

@@ -132,7 +132,7 @@ theorem updates_of_notMem {σ : V → Bool} {vs : List V} {x : V} (hx : x ∉ vs
       rw [updates, ih hx.2, Function.update_of_ne hx.1]
 
 /-- Updating distinct variables by as many values sets them to these values. -/
-theorem map_updates {σ : V → Bool} {vs : List V} (hvs : vs.Nodup) {bs : List Bool}
+private theorem map_updates {σ : V → Bool} {vs : List V} (hvs : vs.Nodup) {bs : List Bool}
     (hlen : bs.length = vs.length) : vs.map (updates σ vs bs) = bs := by
   induction vs generalizing σ bs with
   | nil => exact (List.length_eq_zero_iff.mp hlen).symm
@@ -233,7 +233,7 @@ blocks of level `0`. -/
 def gamePairs (w : ℕ) : List (ℕ × ℕ) :=
   (List.range w).map fun i => (certVar w (2 * i), certVar w (2 * i + 1))
 
-theorem length_gamePairs (w : ℕ) : (gamePairs w).length = w := by
+private theorem length_gamePairs (w : ℕ) : (gamePairs w).length = w := by
   simp [gamePairs]
 
 /-- The variables of the moves are those of the blocks of level `0`. -/
@@ -336,7 +336,7 @@ theorem gameReduce_mem_TQBF_iff {V : α × List Bool → Bool} {kV : ℕ} {State
 def roundTokens (w i : ℕ) : List (QBF.Kind × ℕ) :=
   [(.ex, certVar w (2 * i))] ++ [(.all, certVar w (2 * i + 1))]
 
-theorem tokens_gameFormula {k : ℕ} {State : Type} [Fintype State]
+private theorem tokens_gameFormula {k : ℕ} {State : Type} [Fintype State]
     (tab : CNF (CookLevin.Var k State)) (w : ℕ) :
     (gameFormula tab w).tokens = (List.range w).flatMap (roundTokens w) ++
       (baseFormula tab w).tokens := by
@@ -396,7 +396,7 @@ variable {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × Li
   {A : Set α}
 
 /-- **Games with a polynomial-time winning condition reduce to `TQBF`.** -/
-theorem IsGameVerifier.polyTimeReducible
+private theorem IsGameVerifier.polyTimeReducible
     (hV : ComputableTidilyInPolyTime V (encPair enc encBits) encBool)
     (h : IsGameVerifier enc p V A) : PolyTimeReducible enc encQBF A TQBF := by
   obtain ⟨tV, sV, htV, -, kV, StateV, hfiniteV, tmV, htmV⟩ := hV

Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean

@@ -103,7 +103,8 @@ theorem computableTidilyInPolyTime_sigmaTwoVerifier {W : α × List Bool → Boo
 
 /-- On a proof followed by the shifts and then a random string `r`, the `Σ₂` verifier accepts iff
 `W` accepts the proof with `r` xor some shift. -/
-theorem sigmaTwoVerifier_append_ofFn {q k p : Polynomial ℕ} {W : α × List Bool → Bool} {a : α}
+private theorem sigmaTwoVerifier_append_ofFn {q k p : Polynomial ℕ} {W : α × List Bool → Bool}
+    {a : α}
     {w : List Bool}
     (hw : w.length = q.eval (enc a).length + k.eval (enc a).length * p.eval (enc a).length)
     (r : BitString (p.eval (enc a).length)) :
@@ -193,7 +194,7 @@ theorem computableTidilyInPolyTime_piTwoVerifier {W : α × List Bool → Bool}
 /-- On the shifts followed by any word `v`, the `Π₂` verifier accepts iff `W` accepts, for each
 shift, the first `p(n)` bits of `v` xor the shift with the corresponding reply read from the rest
 of `v`. -/
-theorem piTwoVerifier_append {k p q : Polynomial ℕ} {W : α × List Bool → Bool} {a : α}
+private theorem piTwoVerifier_append {k p q : Polynomial ℕ} {W : α × List Bool → Bool} {a : α}
     {u : List Bool} (hu : u.length = k.eval (enc a).length * p.eval (enc a).length)
     (v : List Bool) :
     piTwoVerifier enc k p q W (a, u ++ v) = true ↔

Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean

@@ -172,7 +172,7 @@ theorem computableTidilyInPolyTime_verifier {N c m T : Polynomial ℕ} {ℓ : α
 /-- On a seed, an element and five certificates, the verifier accepts exactly when the blocks of
 the element have accepted certificates, the padding starts with `ℓ` bits `false` and the affine
 hash given by the seed sends the element to zero. -/
-theorem verifier_ofFn_append {N c m T : Polynomial ℕ} {ℓ : α → ℕ} {R : α × List Bool → Bool}
+private theorem verifier_ofFn_append {N c m T : Polynomial ℕ} {ℓ : α → ℕ} {R : α × List Bool → Bool}
     (a : α) (r : BitString (m.eval (enc a).length * (5 * N.eval (enc a).length +
       T.eval (enc a).length) + m.eval (enc a).length))
     (e : BitString (5 * N.eval (enc a).length + T.eval (enc a).length))

Complexity/Computability/Complexity/Classes/BPP/Derandomization/Generator.lean

@@ -183,14 +183,14 @@ open Turing.MultiTapeTM.ComputableTidilyInPolyTime
 variable {γ : Type} {encIn : γ ↪ List Bool}
 
 /-- Counting the common ones of two masks is polynomial-time. -/
-theorem computableTidilyInPolyTime_overlapCount :
+private theorem computableTidilyInPolyTime_overlapCount :
     ComputableTidilyInPolyTime (fun p : List Bool × List Bool => overlapCount p.1 p.2)
       (encPair encBits encBits) encUnary := by
   unfold overlapCount
   fun_prop
 
 /-- Reading the bits of a word at the ones of a mask is polynomial-time. -/
-theorem computableTidilyInPolyTime_restrictMask :
+private theorem computableTidilyInPolyTime_restrictMask :
     ComputableTidilyInPolyTime (fun p : List Bool × List Bool => restrictMask p.1 p.2)
       (encPair encBits encBits) encBits := by
   unfold restrictMask