refactor(Circuit): make 53 API and general declarations public again in Frontier, Fusion, Monotone and root modules (#926)

Complexity/Computability/Circuit/Approximation.lean

@@ -94,7 +94,7 @@ def programExceptions : ∀ {g : ℕ}, Program σ n g → Finset Sample
   rfl
 
 /-- There are at most as many exceptions as the total cost of the gates. -/
-private theorem card_programExceptions_le {g : ℕ} (p : Program σ n g) :
+theorem card_programExceptions_le {g : ℕ} (p : Program σ n g) :
     (S.programExceptions p).card ≤ p.cost S.errorCost := by
   induction p with
   | empty => simp
@@ -125,7 +125,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. -/
-private theorem circuit_correct {m : ℕ} (C : Circuit σ n m) (o : Fin m) {s : Sample}
+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/Clique.lean

@@ -152,7 +152,7 @@ theorem contains_ofColoring_iff {c : Fin n → Fin r} {s : Finset (Fin n)} :
 
 /-- A set with all edges inside in the graph of a colouring with `r` colours has at most `r`
 vertices. -/
-private theorem card_le_of_contains_ofColoring {c : Fin n → Fin r} {s : Finset (Fin n)}
+theorem card_le_of_contains_ofColoring {c : Fin n → Fin r} {s : Finset (Fin n)}
     (h : Contains (ofColoring c) s) : s.card ≤ r := by
   simpa using Finset.card_le_card_of_injOn c (fun _ _ => Finset.mem_univ _)
     (contains_ofColoring_iff.1 h)

Complexity/Computability/Circuit/Cyclic/Feedback.lean

@@ -55,7 +55,7 @@ def feedbackWire (feed : Fin k → Fin g) : Wire (n + k) g → Wire n g :=
   Wire.elim (Fin.addCases Wire.input (Wire.gate ∘ feed)) Wire.gate
 
 /-- Reading a feedback wire is reading the original wire with the selected gate values as state. -/
-private theorem elim_feedbackWire (feed : Fin k → Fin g) (input : Fin n → U) (state : Fin g → U)
+theorem elim_feedbackWire (feed : Fin k → Fin g) (input : Fin n → U) (state : Fin g → U)
     (wire : Wire (n + k) g) :
     Wire.elim input state (feedbackWire feed wire) =
       Wire.elim (Fin.append input (state ∘ feed)) state wire := by

Complexity/Computability/Circuit/Encoding/MapOp.lean

@@ -29,15 +29,15 @@ namespace Cslib.Circuits
 variable {σ τ : Signature} (φ : σ.Hom τ) {n g m : ℕ}
 
 /-- The code of a translated line: the translated operation on the same wires. -/
-private theorem Line.code_mapOp (line : Line σ n g) :
+theorem Line.code_mapOp (line : Line σ n g) :
     (line.mapOp φ).code = (φ line.op, line.code.2) := by
   simp only [Line.code, Line.mapOp_op, Line.mapOp_wires]
   congr 1
   rw [List.ofFn_congr (φ.arity_eq line.op)]
   simp
 
 /-- The code of a translated program: the operations of its gates translated. -/
-private theorem Program.code_mapOp (p : Program σ n g) :
+theorem Program.code_mapOp (p : Program σ n g) :
     (p.mapOp φ).code = p.code.map fun g => (φ g.1, g.2) := by
   induction p with
   | empty => rfl

Complexity/Computability/Circuit/Erase.lean

@@ -108,7 +108,7 @@ def Program.replaceGates : {s : ℕ} → Program σ n s → (Fin s → Option P)
       ((r (Fin.last _)).elim line.liftConstants Line.const)
 
 /-- The lines of a program with gates replaced by constants. -/
-private theorem Program.lines_replaceGates (p : Program σ n s) (r : Fin s → Option P) (g : Fin s) :
+theorem Program.lines_replaceGates (p : Program σ n s) (r : Fin s → Option P) (g : Fin s) :
     (p.replaceGates r).lines g = (r g).elim (p.lines g).liftConstants Line.const := by
   induction p with
   | empty => exact g.elim0
@@ -137,18 +137,18 @@ theorem Program.lines_eraseGates (p : Program σ n s) (g : Fin s) :
   rw [eraseGates, lines_replaceGates]
   split_ifs <;> rfl
 
-private theorem Program.lines_eraseGates_of_special (p : Program σ n s) {g : Fin s}
+theorem Program.lines_eraseGates_of_special (p : Program σ n s) {g : Fin s}
     (hg : special g) :
     (p.eraseGates special).lines g = Line.const ⟨g, hg⟩ := by
   simp only [lines_eraseGates, hg, ↓reduceDIte]
 
-private theorem Program.lines_eraseGates_of_not_special (p : Program σ n s) {g : Fin s}
+theorem Program.lines_eraseGates_of_not_special (p : Program σ n s) {g : Fin s}
     (hg : ¬special g) : (p.eraseGates special).lines g = (p.lines g).liftConstants := by
   simp only [lines_eraseGates, hg, ↓reduceDIte]
 
 /-- The arity of a gate of the erased program: zero for a special gate, and the arity of the
 gate otherwise. -/
-private theorem Program.arity_lines_eraseGates (p : Program σ n s) (g : Fin s) :
+theorem Program.arity_lines_eraseGates (p : Program σ n s) (g : Fin s) :
     (σ.withConstants {g // special g}).Arity ((p.eraseGates special).lines g).op =
       if special g then 0 else σ.Arity (p.lines g).op := by
   by_cases hg : special g

Complexity/Computability/Circuit/FanIn.lean

@@ -240,7 +240,7 @@ theorem Circuit.essential_le_size
 
 /-- In a program of fan-in `r`, a wire of depth `d` is supported by at most `max 1 r ^ d`
 inputs. -/
-private theorem Program.card_wireSupport_le_pow {r : ℕ} :
+theorem Program.card_wireSupport_le_pow {r : ℕ} :
     ∀ {g : ℕ} {p : Program σ n g}, p.FanInAtMost r →
       ∀ w : Wire n g, (p.wireSupport w).card ≤ max 1 r ^ p.wireDepths w
   | _, .empty, _, .input i => by simp

Complexity/Computability/Circuit/Frontier/AverageCase.lean

@@ -88,7 +88,7 @@ section Finite
 variable [Finite ι] [Finite U]
 
 /-- Membership in `S` agrees with membership in `T` or with membership in `Tᶜ`. -/
-private theorem agreement_add_agreement_compl [Nonempty U] (S T : Set (ι → U)) :
+theorem agreement_add_agreement_compl [Nonempty U] (S T : Set (ι → U)) :
     agreement S T + agreement S Tᶜ = 1 := by
   have hN : (0 : ℝ) < Nat.card (ι → U) := by exact_mod_cast Nat.card_pos
   have hcompl : {x : ι → U | x ∈ S ↔ x ∈ Tᶜ} = {x | x ∈ S ↔ x ∈ T}ᶜ := by

Complexity/Computability/Circuit/Frontier/BranchingProgram.lean

@@ -238,7 +238,7 @@ private theorem smallSides_of_rectangleFree {K : ℕ} (hS : RectangleFree P.acce
 variable {P} in
 /-- Small sides force `K > 1` once some input is accepted: at the first layer both sides of an
 accepted input are nonempty. -/
-private theorem SmallSides.one_lt [Finite ι] [Finite U] {K : ℕ} (hS : P.SmallSides K)
+theorem SmallSides.one_lt [Finite ι] [Finite U] {K : ℕ} (hS : P.SmallSides K)
     (hne : P.accepted.Nonempty) : 1 < K := by
   obtain ⟨x, hx⟩ := hne
   rcases hS 0 (Nat.zero_le _) x hx with h | h

Complexity/Computability/Circuit/Frontier/Layouts/Basic.lean

@@ -41,7 +41,7 @@ namespace Cslib.Circuits.Frontier
 open Set
 
 /-- `log₂ N` is at most `ε N` plus a constant, for every `ε > 0`. -/
-private theorem exists_natLog_le_mul_add {ε : ℝ} (hε : 0 < ε) :
+theorem exists_natLog_le_mul_add {ε : ℝ} (hε : 0 < ε) :
     ∃ K : ℝ, ∀ N : ℕ, (Nat.log 2 N : ℝ) ≤ ε * N + K := by
   obtain ⟨k, hk⟩ := pow_unbounded_of_one_lt (1 / ε) one_lt_two
   refine ⟨k, fun N => ?_⟩

Complexity/Computability/Circuit/Frontier/Layouts/BoundedDegree.lean

@@ -59,7 +59,7 @@ noncomputable def degreeCoefficient (d : ℕ) : ℝ :=
   3 * d / (2 * d - 3) * vertexCoefficient d
 
 /-- The limiting adjacent correlation `2 √(d - 1) / d` is less than one for `d ≥ 3`. -/
-private theorem vertexCorrelation_lt_one {d : ℕ} (hd : 3 ≤ d) : vertexCorrelation d < 1 := by
+theorem vertexCorrelation_lt_one {d : ℕ} (hd : 3 ≤ d) : vertexCorrelation d < 1 := by
   have hD : (3 : ℝ) ≤ d := by exact_mod_cast hd
   have hs : √((d : ℝ) - 1) ^ 2 = d - 1 := sq_sqrt (by linarith)
   rw [vertexCorrelation, div_lt_one (by linarith)]

Complexity/Computability/Circuit/Frontier/Layouts/Gaussian/Basic.lean

@@ -171,15 +171,15 @@ section Deviations
 variable {Ω κ : Type*} [Fintype κ]
 
 /-- The number of events that occur is the sum of their indicators. -/
-private theorem ncard_eq_sum_indicator (A : κ → Set Ω) (ω : Ω) :
+theorem ncard_eq_sum_indicator (A : κ → Set Ω) (ω : Ω) :
     ({k | ω ∈ A k}.ncard : ℝ) = ∑ k, (A k).indicator (1 : Ω → ℝ) ω := by
   classical
   simp only [indicator_apply, Pi.one_apply]
   rw [Finset.sum_boole, ← ncard_coe_finset, Finset.coe_filter_univ]
 
 /-- Outside the event that the number of events that occur deviates from `m` by at least `c`,
 this number is below `m + c`. -/
-private theorem ncard_lt_of_not_le_abs {A : κ → Set Ω} {ω : Ω} {m c : ℝ}
+theorem ncard_lt_of_not_le_abs {A : κ → Set Ω} {ω : Ω} {m c : ℝ}
     (h : ¬c ≤ |∑ k, (A k).indicator (1 : Ω → ℝ) ω - m|) : ({k | ω ∈ A k}.ncard : ℝ) < m + c := by
   rw [ncard_eq_sum_indicator]
   linarith [le_abs_self (∑ k, (A k).indicator (1 : Ω → ℝ) ω - m), not_le.mp h]
@@ -248,7 +248,7 @@ variable {V : Type*} [Fintype V]
 
 /-- The product of standard Gaussians on `V → ℝ` carries an event about inner products to the
 same event under the standard Gaussian measure of `EuclideanSpace ℝ V`. -/
-private theorem measureReal_pi_eq {s : Set (EuclideanSpace ℝ V)} (hs : MeasurableSet s) :
+theorem measureReal_pi_eq {s : Set (EuclideanSpace ℝ V)} (hs : MeasurableSet s) :
     (Measure.pi fun _ : V => gaussianReal 0 1).real {ω | WithLp.toLp 2 ω ∈ s} =
       (stdGaussian (EuclideanSpace ℝ V)).real s :=
   (measurePreserving_toLp_pi_gaussianReal V).measureReal_preimage hs.nullMeasurableSet

Complexity/Computability/Circuit/Frontier/Layouts/General.lean

@@ -60,7 +60,7 @@ def edgeRestrict (F : Set E) : Multigraph V F where
 variable {G}
 
 /-- Removing edges does not increase degrees. -/
-private theorem MaxDegreeLE.edgeRestrict [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (F : Set E) :
+theorem MaxDegreeLE.edgeRestrict [Finite E] {d : ℕ} (hd : G.MaxDegreeLE d) (F : Set E) :
     (G.edgeRestrict F).MaxDegreeLE d := by
   intro v
   rw [← ncard_image_of_injective _ Subtype.val_injective]

Complexity/Computability/Circuit/Frontier/Layouts/Local.lean

@@ -73,7 +73,7 @@ variable {V E : Type*} (G : Multigraph V E)
 
 /-- **Independent sets count edges once.** If no edge has both endpoints in `I`, the edges of
 a set `X` at the vertices of `I` are the disjoint union of those at each vertex of `I`. -/
-private theorem ncard_inter_touching [Finite E] {I : Finset V}
+theorem ncard_inter_touching [Finite E] {I : Finset V}
     (hI : ∀ e, ¬(G.src e ∈ I ∧ G.tgt e ∈ I))
     (X : Set E) : (X ∩ G.touching I).ncard = ∑ v ∈ I, (X ∩ G.incidenceSet v).ncard := by
   classical

Complexity/Computability/Circuit/Frontier/Layouts/Median.lean

@@ -111,14 +111,14 @@ namespace IsMedian
 variable {score : E → α} {v : V} {m : α}
 
 /-- Some edge at `v` scores at most a median. -/
-private theorem exists_score_le (h : G.IsMedian score v m) :
+theorem exists_score_le (h : G.IsMedian score v m) :
     ∃ e ∈ G.incidenceSet v, score e ≤ m := by
   obtain ⟨e, he⟩ := nonempty_of_ncard_ne_zero (s := {e ∈ G.incidenceSet v | score e ≤ m})
     (by have := h.1; omega)
   exact ⟨e, he⟩
 
 /-- Some edge at `v` scores at least a median. -/
-private theorem exists_le_score (h : G.IsMedian score v m) :
+theorem exists_le_score (h : G.IsMedian score v m) :
     ∃ e ∈ G.incidenceSet v, m ≤ score e := by
   obtain ⟨e, he⟩ := nonempty_of_ncard_ne_zero (s := {e ∈ G.incidenceSet v | m ≤ score e})
     (by have := h.2; omega)
@@ -240,7 +240,7 @@ private theorem ncard_edgeCut_le_score_le [Finite V] (h3 : ∀ v, (G.incidenceSe
       (((hP _ hu).trans_lt ht).trans_le hle')
 
 /-- The endpoints of a set of edges number at most twice the edges. -/
-private theorem ncard_endpoints_le (F : Set E) :
+theorem ncard_endpoints_le (F : Set E) :
     {w | ∃ e ∈ F, G.src e = w ∨ G.tgt e = w}.ncard ≤ 2 * F.ncard := by
   refine (ncard_le_ncard (t := G.src '' F ∪ G.tgt '' F) ?_).trans
     ((ncard_union_le _ _).trans ?_)

Complexity/Computability/Circuit/Frontier/LowerBound.lean

@@ -67,7 +67,7 @@ universe u v
 variable {U : Type u} [Finite U] [Nontrivial U]
 
 /-- A set of inputs has at most `|U| ^ n` elements: `log_|U| |S| ≤ n`. -/
-private theorem logb_ncard_le_self {n : ℕ} {S : Set (Fin n → U)} (hS : S.Nonempty) :
+theorem logb_ncard_le_self {n : ℕ} {S : Set (Fin n → U)} (hS : S.Nonempty) :
     Real.logb (Nat.card U) S.ncard ≤ n := by
   have hq : (1 : ℝ) < Nat.card U := by exact_mod_cast Finite.one_lt_card
   have hle : (S.ncard : ℝ) ≤ (Nat.card U : ℝ) ^ n := by

Complexity/Computability/Circuit/Frontier/Multigraph.lean

@@ -249,7 +249,7 @@ theorem edgeCut_union_of_edgeCut_eq_empty {K L : Set V} (hK : G.edgeCut K = ∅)
   · simp [mem_edgeCut, hs, mt hKe.2 hs]
 
 /-- The edges touching a closed set `W` are those with both endpoints in `W`. -/
-private theorem touching_eq_of_edgeCut_eq_empty {W : Set V} (hW : G.edgeCut W = ∅) :
+theorem touching_eq_of_edgeCut_eq_empty {W : Set V} (hW : G.edgeCut W = ∅) :
     G.touching W = {e | G.src e ∈ W ∧ G.tgt e ∈ W} := by
   ext e
   have := G.edgeCut_eq_empty_iff.1 hW e
@@ -259,7 +259,7 @@ private theorem touching_eq_of_edgeCut_eq_empty {W : Set V} (hW : G.edgeCut W =
 /-! ### Connected components -/
 
 /-- The endpoints of an edge lie in the same connected component. -/
-private theorem connectedComponentMk_src (e : E) :
+theorem connectedComponentMk_src (e : E) :
     G.toSimpleGraph.connectedComponentMk (G.src e) =
       G.toSimpleGraph.connectedComponentMk (G.tgt e) :=
   SimpleGraph.ConnectedComponent.sound (G.reachable_src_tgt e)
@@ -308,7 +308,7 @@ theorem MaxDegreeLE.induce [Finite E] {d : ℕ} (hG : G.MaxDegreeLE d) (W : Set
     Subtype.val_injective.injOn).trans (hG w)
 
 /-- The simple graph underlying an induced subgraph is the induced simple graph. -/
-private theorem toSimpleGraph_induce (W : Set V) :
+theorem toSimpleGraph_induce (W : Set V) :
     (G.induce W).toSimpleGraph = G.toSimpleGraph.induce W := by
   ext u v
   simp only [toSimpleGraph_adj, SimpleGraph.comap_adj, Function.Embedding.subtype_apply, ne_eq,

Complexity/Computability/Circuit/Frontier/Network.lean

@@ -431,7 +431,7 @@ theorem unambiguous_branchingProgram
 
 /-- **Edges by width.** At a step that processes a vertex, an edge of the program is determined
 by the values of an assignment on the two frontiers and the inputs read at the vertex. -/
-private theorem ncard_edges_le [Finite ι] [Finite U] [Finite E] {t : ℕ} (ht : t < Nat.card V) :
+theorem ncard_edges_le [Finite ι] [Finite U] [Finite E] {t : ℕ} (ht : t < Nat.card V) :
     ((N.branchingProgram π).edges t).ncard ≤
       Nat.card U ^ ((N.frontier π t ∪ N.frontier π (t + 1)).ncard +
         (N.readAt (π.symm ⟨t, ht⟩)).ncard) := by
@@ -457,7 +457,7 @@ private theorem ncard_edges_le [Finite ι] [Finite U] [Finite E] {t : ℕ} (ht :
 
 /-- At the last step both frontiers are empty, so an edge of the program is determined by the
 unread inputs. -/
-private theorem ncard_edges_last_le [Finite ι] [Finite U] :
+theorem ncard_edges_last_le [Finite ι] [Finite U] :
     ((N.branchingProgram π).edges (Nat.card V)).ncard ≤ Nat.card U ^ N.readᶜ.ncard := by
   have hempty (s : ℕ) (hs : Nat.card V ≤ s) (α : E → U) :
       N.frontierValues π s α = fun _ => none := by

Complexity/Computability/Circuit/Frontier/Nondeterministic.lean

@@ -155,7 +155,7 @@ variable [Finite U] [Nontrivial U]
 /-- **The cycle rank of the graph of a nondeterministic circuit** deciding a large
 `K`-rectangle-free set `S ⊆ U^n` is at most `(r - 1) s - n + log_q K + 1` for fan-in at most `r`,
 where `s` counts the inner gates. Only the `n` ordinary inputs are subtracted. -/
-private theorem cycleRank_le_of_nondeterministicDecides (hfan : c.FanInAtMost r)
+theorem cycleRank_le_of_nondeterministicDecides (hfan : c.FanInAtMost r)
     (hS : c.NondeterministicDecides I Acc S) (hfree : RectangleFree S K)
     (hbig : Nat.card U * K ^ 2 ≤ S.ncard) :
     ((Compiler.graph c).cycleRank : ℝ) ≤
@@ -183,7 +183,7 @@ private theorem cycleRank_le_of_nondeterministicDecides (hfan : c.FanInAtMost r)
 /-- **Every layout of the graph of a nondeterministic circuit is wide.** For a circuit of fan-in
 at most `r ≥ 2` deciding a large `K`-rectangle-free set `S` nondeterministically, every layout `π`
 of its graph satisfies `log_q |S| ≤ width π + (r + 2) + 3 log_q K + log_q (|V| + 1)`. -/
-private theorem logb_ncard_le_width_of_nondeterministicDecides (hr : 2 ≤ r) (hfan : c.FanInAtMost r)
+theorem logb_ncard_le_width_of_nondeterministicDecides (hr : 2 ≤ r) (hfan : c.FanInAtMost r)
     (hS : c.NondeterministicDecides I Acc S) (hfree : RectangleFree S K)
     (hbig : Nat.card U * K ^ 2 ≤ S.ncard) (π : Layout (Compiler.Vertex c)) :
     Real.logb (Nat.card U) S.ncard ≤
@@ -265,7 +265,7 @@ hypothesis for subcubic graphs with coefficient `A > 0`. Under the hypotheses of
 every circuit of fan-in at most two with any number of witness inputs deciding `S_n`
 nondeterministically, over any basis and interpretation on `U`, has more than `(1 + 1/A - ε) n`
 inner gates. -/
-private theorem eventually_lt_innerSize_of_nondeterministicDecides {A : ℝ} (hA : 0 < A)
+theorem eventually_lt_innerSize_of_nondeterministicDecides {A : ℝ} (hA : 0 < A)
     (hlayout : LayoutBound 3 A) (hfree : ∀ᶠ n in atTop, RectangleFree (S n) (K n))
     (hK : (fun n => Real.log (K n)) =o[atTop] fun n => (n : ℝ))
     (hdense : (fun n => n * Real.log (Nat.card U) - Real.log (S n).ncard) =o[atTop]

Complexity/Computability/Circuit/Frontier/Projection.lean

@@ -75,11 +75,11 @@ theorem satisfies_reindex_iff {x : ι' → U} {α : E → U} :
 theorem accepted_reindex : (N.reindex e).accepted = {x | x ∘ e ∈ N.accepted} :=
   rfl
 
-private theorem readAt_reindex (v : V) : (N.reindex e).readAt v = e '' N.readAt v := by
+theorem readAt_reindex (v : V) : (N.reindex e).readAt v = e '' N.readAt v := by
   rw [e.image_eq_preimage_symm]
   rfl
 
-private theorem read_reindex : (N.reindex e).read = e '' N.read := by
+theorem read_reindex : (N.reindex e).read = e '' N.read := by
   rw [e.image_eq_preimage_symm]
   rfl
 

Complexity/Computability/Circuit/Frontier/Rectangle.lean

@@ -294,7 +294,7 @@ theorem signedCount_eq_add_sdiff (S : Set (ι → U)) {R D : Set (ι → U)} (h
   ring
 
 /-- The signed count is twice the deviation of `|R ∩ S|` from `|R| / 2`. -/
-private theorem signedCount_eq_two_mul (S R : Set (ι → U)) :
+theorem signedCount_eq_two_mul (S R : Set (ι → U)) :
     signedCount S R = 2 * (((R ∩ S).ncard : ℝ) - R.ncard / 2) := by
   have : ((R ∩ S).ncard : ℝ) + (R \ S).ncard = R.ncard := by
     exact_mod_cast ncard_inter_add_ncard_sdiff_eq_ncard R S

Complexity/Computability/Circuit/Fusion/Basic.lean

@@ -145,7 +145,7 @@ def Cover.ofProgram (p : Program σ n g) (I : Interpretation σ U) (P : W → U
   (p.cost_eq_sum weight).symm
 
 /-- Every program violating all candidate invariants pays at least the minimum cover cost. -/
-private theorem coverComplexity_le_program_cost (p : Program σ n g) (I : Interpretation σ U)
+theorem coverComplexity_le_program_cost (p : Program σ n g) (I : Interpretation σ U)
     (P : W → U → Prop) (input : Fin n → U) (hin : ∀ t i, P t (input i))
     (hfail : ∀ t, ∃ w, ¬ P t (p.trace I input w)) (weight : σ.Op → ℕ) :
     coverComplexity I P weight ≤ p.cost weight := by

Complexity/Computability/Circuit/Fusion/Converse.lean

@@ -106,7 +106,7 @@ theorem PairCover.exists_forallGuess {n : ℕ} (f : BooleanFunction n)
     exact Formula.eval_toCircuit _ _ _ _
 
 /-- The semi-ultrafilter bound applies after minimizing over all auxiliary counts and verifiers. -/
-private theorem pairCoverComplexity_le_econondeterministicAndComplexity {n : ℕ}
+theorem pairCoverComplexity_le_econondeterministicAndComplexity {n : ℕ}
     (f : BooleanFunction n) :
     pairCoverComplexity {x | f x = true} (fun i => {x | AltFormula.literals x i = true})
       Semifilter.IsUltra ≤ econondeterministicAndComplexity f := by
@@ -116,7 +116,7 @@ private theorem pairCoverComplexity_le_econondeterministicAndComplexity {n : ℕ
   exact pairCoverComplexity_forallGuess_le_cost g c hc
 
 /-- A semi-ultrafilter cover gives a universal verifier at most five times as costly. -/
-private theorem econondeterministicAndComplexity_le_pairCoverComplexity {n : ℕ}
+theorem econondeterministicAndComplexity_le_pairCoverComplexity {n : ℕ}
     (f : BooleanFunction n) :
     econondeterministicAndComplexity f ≤
       5 * pairCoverComplexity {x | f x = true}

Complexity/Computability/Circuit/Fusion/Cyclic.lean

@@ -117,7 +117,7 @@ theorem pairCover_lowerBound_cyclic {target : Set U} {input : Fin n → Set U}
     hbound (PairCover.ofCyclicCircuit c input o hc admissible)
 
 /-- The minimum pair-cover length bounds the AND cost of any cyclic construction. -/
-private theorem pairCoverComplexity_le_cyclic_cost {target : Set U}
+theorem pairCoverComplexity_le_cyclic_cost {target : Set U}
     (c : CyclicCircuit Monotone.signature n m) (input : Fin n → Set U) (o : Fin m)
     (hc : c.eval (Monotone.setInterpretation U) Monotone.setInterpretation_mono input o = target)
     (admissible : Semifilter ↥(targetᶜ) → Prop := fun _ => True) :