refactor(Circuit): privatize 764 module-local proof helpers (#590)

Complexity/Computability/Circuit/Approximation.lean

@@ -92,7 +92,7 @@ def programExceptions : ∀ {g : ℕ}, Program σ n g → Finset Sample
   rfl
 
 /-- There are at most as many exceptions as the total cost of the gates. -/
-theorem card_programExceptions_le {g : ℕ} (p : Program σ n g) :
+private theorem card_programExceptions_le {g : ℕ} (p : Program σ n g) :
     (S.programExceptions p).card ≤ p.cost S.errorCost := by
   induction p with
   | empty => simp
@@ -123,7 +123,7 @@ theorem program_correct {g : ℕ} (p : Program σ n g) {s : Sample}
     | castSucc w => simpa only [Program.trace_gate_castSucc] using ih hs.1 w
 
 /-- Away from the exceptions, every output of a circuit is correct. -/
-theorem circuit_correct {m : ℕ} (C : Circuit σ n m) (o : Fin m) {s : Sample}
+private theorem circuit_correct {m : ℕ} (C : Circuit σ n m) (o : Fin m) {s : Sample}
     (hs : s ∉ S.programExceptions C.program) :
     S.relation (C.eval exact (exactInput s) o) (decode (C.eval approx approxInput o) s) :=
   S.program_correct C.program hs (C.outputs o)

Complexity/Computability/Circuit/Arithmetic/Power.lean

@@ -114,7 +114,7 @@ private theorem binaryPowerCircuit_bit (one : C) (bit : Bool) (e : ℕ) (he : e
 @[simp] theorem binaryMultiplicationCount_one : binaryMultiplicationCount 1 = 0 := by
   simp [binaryMultiplicationCount]
 
-theorem binaryMultiplicationCount_bit (bit : Bool) (e : ℕ) (he : e ≠ 0) :
+private theorem binaryMultiplicationCount_bit (bit : Bool) (e : ℕ) (he : e ≠ 0) :
     binaryMultiplicationCount (Nat.bit bit e) = binaryMultiplicationCount e + 1 + bit.toNat :=
   Nat.binaryRecFromOne_eq bit e he
 

Complexity/Computability/Circuit/Arithmetic/VNP.lean

@@ -82,12 +82,12 @@ noncomputable def booleanSum (m : ℕ) (P : MvPolynomial (Fin (n + m)) K) :
 
 /-- Lift a projection of the first `k` of `k + m` variables to all of them, keeping the last `m`
 variables. -/
-def liftProjection (ρ : Fin k → Fin n ⊕ K) : Fin (k + m) → Fin (n + m) ⊕ K :=
+private def liftProjection (ρ : Fin k → Fin n ⊕ K) : Fin (k + m) → Fin (n + m) ⊕ K :=
   Fin.append (fun i => (ρ i).map (Fin.castAdd m) id) fun i => Sum.inl (Fin.natAdd n i)
 
 /-- A projection of a Boolean sum is the Boolean sum of a projection: substitution for the first
 variables commutes with summing over the last. -/
-theorem projection_booleanSum (ρ : Fin k → Fin n ⊕ K) (P : MvPolynomial (Fin (k + m)) K) :
+private theorem projection_booleanSum (ρ : Fin k → Fin n ⊕ K) (P : MvPolynomial (Fin (k + m)) K) :
     projection ρ (booleanSum m P) = booleanSum m (projection (liftProjection ρ) P) := by
   rw [booleanSum, booleanSum, map_sum]
   refine Finset.sum_congr rfl fun e _ => ?_
@@ -101,7 +101,7 @@ theorem projection_booleanSum (ρ : Fin k → Fin n ⊕ K) (P : MvPolynomial (Fi
   | right i => cases e i <;> simp [booleanAssignment, liftProjection]
 
 /-- A Boolean sum has no larger degree than the summed polynomial. -/
-theorem totalDegree_booleanSum_le (P : MvPolynomial (Fin (n + m)) K) :
+private theorem totalDegree_booleanSum_le (P : MvPolynomial (Fin (n + m)) K) :
     (booleanSum m P).totalDegree ≤ P.totalDegree :=
   totalDegree_finsetSum_le fun _ _ => totalDegree_projection_le _ _
 

Complexity/Computability/Circuit/Arithmetic/VP.lean

@@ -121,7 +121,8 @@ theorem Circuit.aeval_polynomial {R : Type*} [CommSemiring R] [Algebra K R]
 
 /-- Substituting polynomials for the variables of the polynomial computed by a circuit is
 evaluating the circuit at those polynomials. -/
-theorem Circuit.aeval_polynomial_mvPolynomial {σ : Type*} (c : Circuit (arithSignature K) n m)
+private theorem Circuit.aeval_polynomial_mvPolynomial {σ : Type*}
+    (c : Circuit (arithSignature K) n m)
     (x : Fin n → MvPolynomial σ K) (j : Fin m) :
     aeval x (c.polynomial j) = c.eval (arithInterpretationWith K C) x j := by
   rw [c.aeval_polynomial, algebraMap_eq]
@@ -320,7 +321,7 @@ theorem size_projectionCircuit_le (ρ : Fin m → Fin n ⊕ K) : (projectionCirc
 
 /-- Feeding the substitution of a projection to a circuit computes the projection of its
 polynomial. -/
-theorem polynomial_comp_projectionCircuit (c : Circuit (arithSignature K) m p)
+private theorem polynomial_comp_projectionCircuit (c : Circuit (arithSignature K) m p)
     (ρ : Fin m → Fin n ⊕ K) (j : Fin p) :
     (c.comp (projectionCircuit ρ)).polynomial j = projection ρ (c.polynomial j) := by
   rw [projection, Circuit.aeval_polynomial_mvPolynomial, Circuit.polynomial, Circuit.eval_comp]

Complexity/Computability/Circuit/Arithmetic/Waring/Compilation.lean

@@ -77,7 +77,7 @@ theorem Term.eval_toCircuit [Semiring R] (zero one : C) (constant : C → R)
   rfl
 
 /-- Exact weighted term cost, including all coefficient and zero/one constants. -/
-theorem Term.cost_program_toCircuit (zero one : C) (weight : ArithOp C → ℕ) (t : Term C d) :
+private theorem Term.cost_program_toCircuit (zero one : C) (weight : ArithOp C → ℕ) (t : Term C d) :
     (t.toCircuit zero one).program.cost weight =
       weight (.const zero) +
         (∑ i, (weight (.const (t.coefficients i)) + weight .mul + weight .add)) +
@@ -92,13 +92,13 @@ theorem Term.cost_program_toCircuit (zero one : C) (weight : ArithOp C → ℕ)
 def termMultiplicationCount (d : ℕ) : ℕ := d + binaryMultiplicationCount d + 1
 
 /-- Exact term multiplication count, including the final scale multiplication at degree zero. -/
-theorem Term.mulCost_toCircuit (zero one : C) (t : Term C d) :
+private theorem Term.mulCost_toCircuit (zero one : C) (t : Term C d) :
     (t.toCircuit zero one).program.cost ArithOp.mulCost = termMultiplicationCount d := by
   rw [Term.cost_program_toCircuit]
   by_cases hd : d = 0 <;> simp [ArithOp.mulCost, termMultiplicationCount, hd]
 
 /-- There is one linear-form addition per variable, including the initial addition to zero. -/
-theorem Term.addCost_toCircuit (zero one : C) (t : Term C d) :
+private theorem Term.addCost_toCircuit (zero one : C) (t : Term C d) :
     (t.toCircuit zero one).program.cost ArithOp.addCost = d := by
   rw [Term.cost_program_toCircuit]
   simp [ArithOp.addCost]
@@ -181,7 +181,7 @@ theorem cost_program_compile (zero one : C)
   | term t => exact t.cost_program_toCircuit zero one weight
 
 /-- Uniform term costs separate the total charge into source additions and term gates. -/
-theorem cost_program_compile_of_termCost (zero one : C)
+private theorem cost_program_compile_of_termCost (zero one : C)
     (c : Circuit (SumOfTerms.signature (Term C d)) n m) (weight : ArithOp C → ℕ) {term : ℕ}
     (hterm : ∀ t : Term C d, (t.toCircuit zero one).program.cost weight = term) :
     (compile zero one c).program.cost weight =

Complexity/Computability/Circuit/Boolean/ACC0.lean

@@ -73,7 +73,7 @@ namespace Cslib.Circuits.Boolean
 open Set Finset BitString Unbounded Cslib.Complexity Turing.MultiTapeTM
 
 /-- Folding `xor` over a Boolean word computes `parity` of its slice. -/
-theorem foldl_bne_eq_parity (w : List Bool) :
+private theorem foldl_bne_eq_parity (w : List Bool) :
     w.foldl bne false = parity w.length (fun i => w[i]) := by
   have hcount : w.foldl bne false = decide (w.count true % 2 = 1) := by
     have hgen (b : Bool) (l : List Bool) :

Complexity/Computability/Circuit/Boolean/AffineDisperser.lean

@@ -115,7 +115,7 @@ theorem initialState_valid {C : Circuit (fullSignature 2 Bool) n 1}
 theorem initialState_a (C : Circuit (fullSignature 2 Bool) n 1) : (initialState C).a = n := by
   simp [State.a, State.m, State.q, initialState]
 
-theorem initialState_W_le (C : Circuit (fullSignature 2 Bool) n 1) :
+private theorem initialState_W_le (C : Circuit (fullSignature 2 Bool) n 1) :
     (initialState C).W ≤ 2 * C.size + 7 * n := by
   have hs : (initialState C).s = C.size := by
     simp [State.s, SemiCircuit.size, initialState]

Complexity/Computability/Circuit/Boolean/AffineDisperser/Deletion.lean

@@ -153,7 +153,7 @@ theorem Valid.unit_delete {S : State n} {d : ℕ} (hS : S.Valid f) (hf : IsAffin
   exact ⟨S', hS', hm, hs, ha', hq, by omega⟩
 
 /-- (D4) as a step of gate elimination. -/
-theorem Valid.step_unit {S : State n} {d : ℕ} (hS : S.Valid f) (hf : IsAffineDisperser f d)
+private theorem Valid.step_unit {S : State n} {d : ℕ} (hS : S.Valid f) (hf : IsAffineDisperser f d)
     (ha : d < S.a) {x e : ℕ} (hx : x ∈ S.unpaired) (hc : S.children x = {.inr e}) :
     ∃ S', Step f S S' := by
   obtain ⟨S', hS', hm, hs, ha', -, hW⟩ := hS.unit_delete hf ha hx hc

Complexity/Computability/Circuit/Boolean/AffineDisperser/Elimination.lean

@@ -64,7 +64,7 @@ def SharedSecondChild (S : State n) (G x y : ℕ) : Prop :=
 
 /-- Restricting one input `x'` of the minimal AND and deleting its two children `G` and `B`,
 which are also the children of the other input `y'`, is a step: `Δa = -1`, `ΔW ≤ -18`. -/
-theorem Reduction.step_of_shared {S S' : State n} (hS : S.Valid f) {G x' y' : ℕ}
+private theorem Reduction.step_of_shared {S S' : State n} (hS : S.Valid f) {G x' y' : ℕ}
     {B : ℕ ⊕ ℕ} (hx' : x' ∈ S.unpaired) (hy' : y' ∈ S.unpaired) (hxy : x' ≠ y')
     (hx'2 : S.deg x' = 2) (hy'2 : S.deg y' = 2) (hcy : S.children y' = {.inl G, B})
     (h : Reduction f S S' {x'} [.inl G, B] []) : Step f S S' := by
@@ -90,7 +90,7 @@ theorem Reduction.step_of_shared {S S' : State n} (hS : S.Valid f) {G x' y' : 
 /-- Restricting a parameter `x'` to a constant or to a literal of another parameter with at least
 its children, on which the gates `G` and `B ≠ G`, `B` not reading `G`, are constant, and deleting
 both gates, is a reduction. -/
-theorem Valid.exists_reduction_restrict_deleteConst {S : State n} (hS : S.Valid f) {x' : ℕ}
+private theorem Valid.exists_reduction_restrict_deleteConst {S : State n} (hS : S.Valid f) {x' : ℕ}
     (hx' : x' ∈ S.params) {ℓ : Lit} (hℓ : ∀ t, ℓ.Reads t → t ∈ S.params ∧ t ≠ x' ∧
       S.children x' ⊆ S.children t ∧ (S.Paired x' → S.IsPartner x' t))
     {G B : ℕ} (hG : G ∈ S.gates) (hB : B ∈ S.gates) (hBG : B ≠ G)
@@ -114,7 +114,7 @@ theorem Valid.exists_reduction_restrict_deleteConst {S : State n} (hS : S.Valid
 
 /-- Case 7 when the shared second child `B` of `x` and `y` is a gate: on one of the lines `x = c`,
 `y = c` or `x = y + c` both `G` and `B` are constant, and restricting to it deletes both. -/
-theorem Valid.exists_reduction_sharedGate {S : State n} (hS : S.Valid f) {G x y B : ℕ}
+private theorem Valid.exists_reduction_sharedGate {S : State n} (hS : S.Valid f) {G x y B : ℕ}
     (h : S.MinimalAnd G x y) (hcx : S.children x = {.inl G, .inl B})
     (hcy : S.children y = {.inl G, .inl B}) (hBG : B ≠ G) :
     ∃ S' x' y', ((x' = x ∧ y' = y) ∨ (x' = y ∧ y' = x)) ∧
@@ -163,7 +163,7 @@ theorem Valid.exists_reduction_sharedGate {S : State n} (hS : S.Valid f) {G x y
 /-- Case 7 when the shared second child of `x` and `y` is an equation `v + x + y = rhs`:
 restricting to the line `x = y + c` on which `G` is constant makes the equation read `v = rhs + c`,
 and both are deleted. -/
-theorem Valid.exists_reduction_sharedEqn {S : State n} (hS : S.Valid f) (hN : S.Normal)
+private theorem Valid.exists_reduction_sharedEqn {S : State n} (hS : S.Valid f) (hN : S.Normal)
     {G x y e : ℕ} (h : S.MinimalAnd G x y) (hcx : S.children x = {.inl G, .inr e})
     (hcy : S.children y = {.inl G, .inr e}) :
     ∃ S', Reduction f S S' {x} [.inl G, .inr e] [] := by
@@ -283,7 +283,7 @@ def fixInputDeleted (S : State n) (G x : ℕ) : Finset (ℕ ⊕ ℕ) :=
 /-- Fixing the input `x` of the minimal AND so that `G` becomes constant, and deleting `G`, the
 other children of `x` and the children of `G`, is a reduction deleting `deg x + deg G`
 constraints. -/
-theorem Valid.exists_reduction_fixInput {S : State n} (hS : S.Valid f) {G x y : ℕ}
+private theorem Valid.exists_reduction_fixInput {S : State n} (hS : S.Valid f) {G x y : ℕ}
     (h : S.MinimalAnd G x y) : ∃ S', Reduction f S S' {x}
       (.inl G :: (S.fixInputDeleted G x).toList) (S.fixInputDeleted G x).toList := by
   have hxG := h.ne_gate hS h.mem_params_x
@@ -302,7 +302,7 @@ theorem Valid.exists_reduction_fixInput {S : State n} (hS : S.Valid f) {G x y :
         (by rw [fixConst_gate, Gate.reads_subst_of_ne hxG.symm (by simp [Lit.const])]; exact hKG)
   exact ⟨S', (h₁.trans_delete h₂).trans_delete h₃⟩
 
-theorem MinimalAnd.length_fixInput {S : State n} (hS : S.Valid f) {G x y : ℕ}
+private theorem MinimalAnd.length_fixInput {S : State n} (hS : S.Valid f) {G x y : ℕ}
     (h : S.MinimalAnd G x y) :
     (Sum.inl G :: (S.fixInputDeleted G x).toList).length = S.deg x + S.deg G := by
   have hdisj : Disjoint ((S.children x).erase (.inl G)) (S.children G) := by
@@ -378,7 +378,7 @@ theorem Reduction.wt_add_le_fixInput {S S' : State n} (hS : S.Valid f) (hN : S.N
 
 /-- Outside the bottleneck configuration, when `deg x = 2` and `G` has one child, no unpaired
 isolated parameter lies below `G`. -/
-theorem MinimalAnd.not_isolatedBelow {S : State n} (hS : S.Valid f) {G x y : ℕ}
+private theorem MinimalAnd.not_isolatedBelow {S : State n} (hS : S.Valid f) {G x y : ℕ}
     (h : S.MinimalAnd G x y) (hbot : ¬ S.Bottleneck G x) (hx2 : S.deg x = 2)
     (hG1 : S.deg G = 1) {u : ℕ} : ¬ S.IsolatedBelow G u := fun ⟨hu1, hu2, N, hNG, hNu⟩ => by
   refine hbot ⟨hx2, ?_⟩
@@ -434,7 +434,7 @@ theorem Valid.step_fixInput {S : State n} (hS : S.Valid f) (hN : S.Normal) {G x
 
 /-- The weights after the quadratic reparameterisation: `x` and `y` become paired, `z` is
 replaced by `D`, which gains at most seven, and no other weight grows. -/
-theorem QuadOK.wt_add_le {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β γ c : Bool}
+private theorem QuadOK.wt_add_le {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β γ c : Bool}
     (h : S.QuadOK x y z G D α β γ c) (hx : 2 ≤ S.deg x) (hy : 2 ≤ S.deg y) :
     ∀ u ∈ insert D S.params, (S.quad x y z G D α β γ c).wt u + ((if u = x then 7 else 0) +
       (if u = y then 7 else 0) + (if u = z then 6 else 0)) ≤ S.wt u + (if u = D then 7 else 0) := by
@@ -484,7 +484,7 @@ theorem QuadOK.wt_add_le {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β
 
 /-- The quadratic reparameterisation of the bottleneck configuration, when `x` and `y` have
 degree at least two, is a step of gate elimination: `Δa = -1`, `ΔW ≤ -14`. -/
-theorem Valid.step_quad {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β γ c : Bool}
+private theorem Valid.step_quad {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β γ c : Bool}
     (h : S.QuadOK x y z G D α β γ c) (hx : 2 ≤ S.deg x) (hy : 2 ≤ S.deg y) :
     Step f S (S.quad x y z G D α β γ c) := by
   set S' := S.quad x y z G D α β γ c
@@ -509,7 +509,7 @@ theorem Valid.step_quad {S : State n} (hS : S.Valid f) {x y z G D : ℕ} {α β
     by simp only [State.a]; omega⟩
 
 /-- In the bottleneck configuration, `G` has the unique child `D` and `z` the unique child `D`. -/
-theorem MinimalAnd.children_of_bottleneck {S : State n} (hS : S.Valid f) {G x y D z : ℕ}
+private theorem MinimalAnd.children_of_bottleneck {S : State n} (hS : S.Valid f) {G x y D z : ℕ}
     (h : S.MinimalAnd G x y) (hDiff : ∀ K ∈ S.gates, (S.gate K).Reads G ↔ K = D)
     (hD : D ∈ S.gates) (hz1 : S.deg z = 1) (hDz : (S.gate D).Reads z) :
     S.children G = {.inl D} ∧ S.children z = {.inl D} := by
@@ -527,7 +527,7 @@ theorem MinimalAnd.children_of_bottleneck {S : State n} (hS : S.Valid f) {G x y
 
 /-- In the bottleneck configuration with `D` AND-type, fixing `x` and `y` so that `G` takes the
 value making `D` constant deletes `G`, `D` and the second children `Bx`, `By` of `x` and `y`. -/
-theorem Valid.exists_reduction_bottleneck_and {S : State n} (hS : S.Valid f) {G x y D : ℕ}
+private theorem Valid.exists_reduction_bottleneck_and {S : State n} (hS : S.Valid f) {G x y D : ℕ}
     (h : S.MinimalAnd G x y) (hD : D ∈ S.gates) (hDG' : D ≠ G)
     {δ c : Bool} (hc : ∀ val : ℕ → Bool, val G = δ → (S.gate D).eval val = c)
     {x₀ y₀ : Bool} (hδ : (S.gate G).eval (Function.update (Function.update (fun _ => false) y y₀)
@@ -674,7 +674,7 @@ theorem Valid.step_of_bottleneck_xor {S : State n} {d : ℕ} (hS : S.Valid f)
 /-- **Cases 9 and 10** of [Mishra and Santhanam, Section 4.3][MishraSanthanam2026], the
 bottleneck configuration: the unique child `D` of the minimal AND `G` reads an unpaired isolated
 parameter `z`; its elimination is a step. -/
-theorem Valid.step_of_bottleneck {S : State n} {d : ℕ} (hS : S.Valid f)
+private theorem Valid.step_of_bottleneck {S : State n} {d : ℕ} (hS : S.Valid f)
     (hf : IsAffineDisperser f d) (ha : d < S.a) (hN : S.Normal) {G x y : ℕ}
     (h : S.MinimalAnd G x y) (h7 : ¬ S.SharedSecondChild G x y) (hbot : S.Bottleneck G x) :
     ∃ S', Step f S S' := by