refactor(Circuit/Rational,Arithmetic): make 51 API and general declarations public again (#926)

Complexity/Computability/Circuit/Arithmetic/Power.lean

@@ -119,7 +119,7 @@ private theorem binaryPowerCircuit_bit (one : C) (bit : Bool) (e : ℕ) (he : e
 @[simp] theorem binaryMultiplicationCount_one : binaryMultiplicationCount 1 = 0 := by
   simp [binaryMultiplicationCount]
 
-private theorem binaryMultiplicationCount_bit (bit : Bool) (e : ℕ) (he : e ≠ 0) :
+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

@@ -101,7 +101,7 @@ private theorem projection_booleanSum (ρ : Fin k → Fin n ⊕ K) (P : MvPolyno
   | right i => cases e i <;> simp [booleanAssignment, liftProjection]
 
 /-- A Boolean sum has no larger degree than the summed polynomial. -/
-private theorem totalDegree_booleanSum_le (P : MvPolynomial (Fin (n + m)) K) :
+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,7 @@ 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. -/
-private theorem Circuit.aeval_polynomial_mvPolynomial {σ : Type*}
+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
@@ -325,7 +325,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. -/
-private theorem polynomial_comp_projectionCircuit (c : Circuit (arithSignature K) m p)
+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

@@ -79,7 +79,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. -/
-private theorem Term.cost_program_toCircuit (zero one : C) (weight : ArithOp C → ℕ) (t : Term C d) :
+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)) +
@@ -94,13 +94,13 @@ private 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. -/
-private theorem Term.mulCost_toCircuit (zero one : C) (t : Term C d) :
+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. -/
-private theorem Term.addCost_toCircuit (zero one : C) (t : Term C d) :
+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]

Complexity/Computability/Circuit/Rational/EncodingBounds.lean

@@ -67,12 +67,12 @@ private lemma encodeNat_le (a L : ℕ) (ha : a < 2 ^ L) : (encodeNat a).length 
   exact Nat.add_le_add_right (Nat.mul_le_mul_left 2 ((Nat.digits_length_le_iff (by omega) a).mpr
     ha)) 1
 
-private lemma ratio_num_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs ≤ a.natAbs := by
+lemma ratio_num_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs ≤ a.natAbs := by
   by_cases ha : a = 0
   · simp [ha]
   · exact Int.natAbs_le_of_dvd_ne_zero (Rat.num_dvd a hb) ha
 
-private lemma ratio_den_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den ≤ b.natAbs := by
+lemma ratio_den_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den ≤ b.natAbs := by
   simpa only [Int.natAbs_natCast] using Int.natAbs_le_of_dvd_ne_zero (Rat.den_dvd a b) hb
 
 private lemma encodeRat_ratio_le (a b : ℤ) (hb : b ≠ 0) (L : ℕ)
@@ -83,7 +83,7 @@ private lemma encodeRat_ratio_le (a b : ℤ) (hb : b ≠ 0) (L : ℕ)
   simp only [encodeRat, List.length_append, List.length_singleton]
   omega
 
-private lemma determinant_bound {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) (B : ℕ)
+lemma determinant_bound {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) (B : ℕ)
     (hA : ∀ i j, |A i j| ≤ B) : |A.det| ≤ (d.factorial : ℤ) * (B : ℤ) ^ d := by
   have h := Matrix.det_le (abv := AbsoluteValue.abs) (x := (B : ℤ)) (A := A) (by simpa using hA)
   simpa only [AbsoluteValue.abs_apply, nsmul_eq_mul, Fintype.card_fin] using h

Complexity/Computability/Circuit/Rational/Eval.lean

@@ -152,14 +152,14 @@ abbrev matMul {l m n : Type*} [Fintype m] (A : Matrix l m R) (B : Matrix m n R)
     Matrix l n R := A * B
 
 /-- An upper unitriangular block matrix is invertible. -/
-private theorem upper_unit (B : Matrix ι κ R) :
+theorem upper_unit (B : Matrix ι κ R) :
     IsUnit (fromBlocks (1 : Matrix ι ι R) B 0 (1 : Matrix κ κ R)) := by
   apply isUnit_iff_exists.mpr
   refine ⟨fromBlocks 1 (-B) 0 1, ?_, ?_⟩ <;>
     simp [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul]
 
 /-- A lower unitriangular block matrix is invertible. -/
-private theorem lower_unit (C : Matrix κ ι R) :
+theorem lower_unit (C : Matrix κ ι R) :
     IsUnit (fromBlocks (1 : Matrix ι ι R) 0 C (1 : Matrix κ κ R)) := by
   apply isUnit_iff_exists.mpr
   refine ⟨fromBlocks 1 0 (-C) 1, ?_, ?_⟩ <;>
@@ -201,7 +201,7 @@ theorem diag_unit_iff (A : Matrix ι ι R) (D : Matrix κ κ R) :
       simp [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul]
 
 /-- The Schur factorization of a block matrix with a zero corner and an invertible corner. -/
-private theorem schur_factor (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R)
+theorem schur_factor (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R)
     (hAA' : A * A' = 1) (hA'A : A' * A = 1) :
     fromBlocks A B C 0 =
       fromBlocks 1 0 (C * A') 1 * fromBlocks A 0 0 (-C * A' * B) *

Complexity/Computability/Circuit/Rational/Generator.lean

@@ -242,7 +242,7 @@ private lemma condition_degree {n s N e : ℕ} (hs : 1 ≤ s) (f : Formula n) (h
         gcongr
         exact ((Formula.certificate_bounds f s hs hf).2 h hh).2)
 
-private lemma integer_grid {K : Type*} [Field K] [CharZero K] (P : List (MvPolynomial (Fin 3) K))
+lemma integer_grid {K : Type*} [Field K] [CharZero K] (P : List (MvPolynomial (Fin 3) K))
     (hP : ∀ p ∈ P, p ≠ 0) (d H : ℕ) (hd : ∀ p ∈ P, p.totalDegree ≤ d)
     (hH : P.length * d < H) :
     ∃ x : Fin 3 → Fin H, ∀ p ∈ P, eval (fun i => (((x i).val + 1 : ℕ) : K)) p ≠ 0 := by

Complexity/Computability/Circuit/Rational/IntegralLift.lean

@@ -396,7 +396,7 @@ lemma U_bound (n N e H : ℕ) (x : Fin 3 → ℕ) (hH : 1 ≤ H) (hx : ∀ l, x
     CyclotomicRing.dimension e + 2 * CyclotomicRing.dimension e by omega, pow_add]
   ring
 
-private lemma scaled_normalization {d : ℕ} (A B : Mat d) (hA : A.det ≠ 0) (c : ℚ) (hc : c ≠ 0) :
+lemma scaled_normalization {d : ℕ} (A B : Mat d) (hA : A.det ≠ 0) (c : ℚ) (hc : c ≠ 0) :
     (c • A)⁻¹ * (c • B) = A⁻¹ * B := by
   let : Invertible c := invertibleOfNonzero hc
   have hi : (c • A)⁻¹ = c⁻¹ • A⁻¹ := by

Complexity/Computability/Circuit/Rational/LaurentReduction.lean

@@ -488,7 +488,7 @@ private theorem reduction_weighted_supported {ι : Type*} [Finite ι]
   exact he ▸ weighted_high_reduction_zero w A (u • x) hnI' hd u⁻¹
     (inv_ne_zero hu) (he.symm ▸ hyI)
 
-private lemma exists_independent_subfamily {V : Type*} [AddCommGroup V] [Module K V]
+lemma exists_independent_subfamily {V : Type*} [AddCommGroup V] [Module K V]
     {h : ℕ} (v : Fin h → V) :
     ∃ (k : ℕ) (a : Fin k → Fin h), Function.Injective a ∧
       Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧

Complexity/Computability/Circuit/Rational/MatrixEval.lean

@@ -50,11 +50,11 @@ namespace Cslib.Circuits.Rational
 
 open Rational.Formula Rational.Output
 
-private theorem matrix_inverse_left {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) :
+theorem matrix_inverse_left {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) :
     a * (a.det⁻¹ • a.adjugate) = 1 := by
   rw [Matrix.mul_smul, Matrix.mul_adjugate, smul_smul, inv_mul_cancel₀ ha, one_smul]
 
-private theorem matrix_inverse_right {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) :
+theorem matrix_inverse_right {d : ℕ} (a : Mat d) (ha : a.det ≠ 0) :
     (a.det⁻¹ • a.adjugate) * a = 1 := by
   rw [Matrix.smul_mul, Matrix.adjugate_mul, smul_smul, inv_mul_cancel₀ ha, one_smul]
 

Complexity/Computability/Circuit/Rational/QuantumMatrices.lean

@@ -57,7 +57,7 @@ open scoped BigOperators
 noncomputable section
 variable {Γ R : Type*} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R]
 
-private lemma coeff_mul_support_superset (x y : HahnSeries Γ R) (a : Γ)
+lemma coeff_mul_support_superset (x y : HahnSeries Γ R) (a : Γ)
     (s t : Set Γ) (hs : s.IsPWO) (ht : t.IsPWO)
     (hxs : x.support ⊆ s) (hyt : y.support ⊆ t) :
     (x * y).coeff a = ∑ ij ∈ Finset.antidiagonal hs ht a,

Complexity/Computability/Circuit/Rational/QuantumSeries.lean

@@ -144,7 +144,7 @@ open HahnSeries HahnSeries.SummableFamily Finset Function
 noncomputable section
 variable {Γ R : Type*} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R]
 
-private theorem power_finite_co_support {x : R⟦Γ⟧} (hx : 0 < x.orderTop) (g : Γ) :
+theorem power_finite_co_support {x : R⟦Γ⟧} (hx : 0 < x.orderTop) (g : Γ) :
     Set.Finite {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0} := by
   have hpwo : Set.IsPWO (⋃ n, support (x ^ n)) :=
     isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt hx)

Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean

@@ -236,7 +236,7 @@ private lemma sum_map_drop_range (d lo : ℕ) (f : ℕ → ℤ) :
     rw [BirdDet.sumFrom_stop d lo f hlo, List.drop_eq_nil_of_le (by simpa using hlo)]
     rfl
 
-private lemma sum_map_drop_range_fin {d : ℕ} (i : Fin d) (f : ℕ → ℤ) :
+lemma sum_map_drop_range_fin {d : ℕ} (i : Fin d) (f : ℕ → ℤ) :
     (((List.range d).drop (i.val + 1)).map f).sum = ∑ k ∈ Finset.Ioi i, f k.val := by
   rw [sum_map_drop_range, DeterminantAlgorithm.sumFrom_fin_tail]
 
@@ -300,7 +300,7 @@ theorem detRows_rowsOf_denote {d : ℕ} (A : DeterminantAlgorithm.Table d) :
 
 /-! ### Size bounds -/
 
-private lemma natAbs_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) :
+lemma natAbs_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) :
     l.sum.natAbs ≤ l.length * C := by
   induction l with
   | nil => simp
@@ -312,7 +312,7 @@ private lemma natAbs_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs
       _ = (l.length + 1) * C := by ring
 
 /-- Every prefix sum of a list is bounded by its length times a bound on its entries. -/
-private lemma natAbs_take_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) (m : ℕ) :
+lemma natAbs_take_sum_le {l : List ℤ} {C : ℕ} (h : ∀ x ∈ l, x.natAbs ≤ C) (m : ℕ) :
     (l.take m).sum.natAbs ≤ l.length * C :=
   (natAbs_sum_le fun x hx => h x (List.mem_of_mem_take hx)).trans
     (Nat.mul_le_mul_right _ (List.length_take_le' _ _))

Complexity/Computability/Circuit/Rational/Runtime/Encode.lean

@@ -125,23 +125,23 @@ theorem divInt_sign (a b : ℤ) (hb : b ≠ 0) :
       simp [not_lt_of_gt hpa, not_lt_of_gt hpb, not_lt_of_ge hp.le]
 
 /-- Reduced numerator magnitude of `Rat.divInt a b` for arbitrary integers `a, b`. -/
-private theorem divInt_num_abs_eq (a b : ℤ) :
+theorem divInt_num_abs_eq (a b : ℤ) :
     (Rat.divInt a b).num.natAbs =
       if b = 0 then 0 else a.natAbs / Nat.gcd a.natAbs b.natAbs := by
   by_cases hb : b = 0
   · subst hb; simp
   · simp [hb, divInt_num_abs a b hb]
 
 /-- Reduced denominator of `Rat.divInt a b` for arbitrary integers `a, b`. -/
-private theorem divInt_den_eq (a b : ℤ) :
+theorem divInt_den_eq (a b : ℤ) :
     (Rat.divInt a b).den =
       if b = 0 then 1 else b.natAbs / Nat.gcd a.natAbs b.natAbs := by
   by_cases hb : b = 0
   · subst hb; simp
   · simp [hb, divInt_den a b hb]
 
 /-- Sign bit of `Rat.divInt a b` for arbitrary integers `a, b`. -/
-private theorem divInt_sign_eq (a b : ℤ) :
+theorem divInt_sign_eq (a b : ℤ) :
     decide ((Rat.divInt a b).num < 0) =
       if a = 0 then false else if b = 0 then false else (decide (a < 0) ^^ decide (b < 0)) := by
   by_cases hb : b = 0

Complexity/Computability/Circuit/Rational/Runtime/Lift.lean

@@ -66,7 +66,7 @@ namespace Rational
 
 /-! ### Magnitude bounds -/
 
-private lemma natAbs_pow_le {z : ℤ} {H : ℕ} (hH : 1 ≤ H) (hz : z.natAbs ≤ H) {q M : ℕ}
+lemma natAbs_pow_le {z : ℤ} {H : ℕ} (hH : 1 ≤ H) (hz : z.natAbs ≤ H) {q M : ℕ}
     (hq : q ≤ M) :
     (z ^ q).natAbs ≤ H ^ M := by
   rw [Int.natAbs_pow]

Complexity/Computability/Circuit/Rational/Runtime/Lift/Defs.lean

@@ -77,7 +77,7 @@ open Polynomial
 
 /-! ### Index bridges -/
 
-private lemma val_finEquiv {m : ℕ} [NeZero m] (i : Fin m) : (ZMod.finEquiv m i).val = i.val := by
+lemma val_finEquiv {m : ℕ} [NeZero m] (i : Fin m) : (ZMod.finEquiv m i).val = i.val := by
   cases m with
   | zero => exact (NeZero.ne 0 rfl).elim
   | succ m => rfl
@@ -88,21 +88,21 @@ lemma val_finEquiv_symm {m : ℕ} [NeZero m] (z : ZMod m) :
   rw [← val_finEquiv, RingEquiv.apply_symm_apply]
 
 /-- A sum over `List.range m` is a sum over `Fin m`. -/
-private lemma sum_range_eq_sum_fin {A : Type*} [AddCommMonoid A] (m : ℕ) (f : ℕ → A) :
+lemma sum_range_eq_sum_fin {A : Type*} [AddCommMonoid A] (m : ℕ) (f : ℕ → A) :
     ((List.range m).map f).sum = ∑ i : Fin m, f i := by
   rw [← List.map_coe_finRange_eq_range, List.map_map, ← List.ofFn_eq_map, List.sum_ofFn]
   rfl
 
 /-- A sum over `List.range m` is a sum over the residues modulo `m`. -/
-private lemma sum_range_eq_sum_zmod {A : Type*} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ℕ → A) :
+lemma sum_range_eq_sum_zmod {A : Type*} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ℕ → A) :
     ((List.range m).map f).sum = ∑ z : ZMod m, f z.val := by
   rw [sum_range_eq_sum_fin]
   exact Fintype.sum_equiv (ZMod.finEquiv m).toEquiv _ _ fun i => by
     change f i.val = f (ZMod.finEquiv m i).val
     rw [val_finEquiv]
 
 /-- Residue subtraction on values, without truncated subtraction below zero. -/
-private lemma val_sub_eq_mod {m : ℕ} [NeZero m] (u v : ZMod m) :
+lemma val_sub_eq_mod {m : ℕ} [NeZero m] (u v : ZMod m) :
     (u - v).val = (u.val + m - v.val) % m := by
   have hv := v.val_lt
   rw [← ZMod.val_natCast, Nat.cast_sub (by omega), Nat.cast_add, ZMod.natCast_self,

Complexity/Computability/Circuit/Rational/SmallExpansion.lean

@@ -280,7 +280,7 @@ theorem order_reversal_sum (M : ℕ) (a : K)
       Fintype.card_fin, smul_eq_mul]
   omega
 
-private lemma sum_fin_val_le_square (h : ℕ) : (∑ j : Fin h, j.val) ≤ h * h := by
+lemma sum_fin_val_le_square (h : ℕ) : (∑ j : Fin h, j.val) ≤ h * h := by
   calc
     _ ≤ ∑ _j : Fin h, h := Finset.sum_le_sum fun j _ => Nat.le_of_lt j.isLt
     _ = h * h := by simp