refactor(classes): make proof helpers private, second pass

Complexity/Computability/Complexity/AffineDisperser/PolyTime.lean

@@ -84,7 +84,7 @@ theorem computableTidilyInPolyTime_mulXMod :
   unfold mulXMod
   fun_prop
 
-theorem length_mulXMod_le (g r : List Bool) : (mulXMod g r).length ≤ g.length - 1 :=
+private theorem length_mulXMod_le (g r : List Bool) : (mulXMod g r).length ≤ g.length - 1 :=
   List.length_take_le _ _
 
 /-- The remainder modulo a binary polynomial, by a left fold over the coefficients whose state, the
@@ -150,7 +150,7 @@ theorem computableTidilyInPolyTime_powerTable :
 /-! ### Lists of unary naturals -/
 
 /-- Take a unary number of elements of a framed list, by reversing and dropping. -/
-theorem computableTidilyInPolyTime_take {α : Type} (enc : α ↪ List Bool) :
+private theorem computableTidilyInPolyTime_take {α : Type} (enc : α ↪ List Bool) :
     ComputableTidilyInPolyTime (fun p : List α × ℕ => p.1.take p.2)
       (encPair (encList enc) encUnary) (encList enc) := by
   have hrev := (listReverse enc).comp (fst (encList enc) encUnary)
@@ -163,7 +163,8 @@ theorem computableTidilyInPolyTime_take {α : Type} (enc : α ↪ List Bool) :
 
 /-- The product of a computed list of positive unary naturals, when the product is polynomially
 bounded: every partial product is at most the whole product. -/
-theorem computableTidilyInPolyTime_prod_of_le {α : Type} {input : α ↪ List Bool} {list : α → List ℕ}
+private theorem computableTidilyInPolyTime_prod_of_le {α : Type} {input : α ↪ List Bool}
+    {list : α → List ℕ}
     (hlist : ComputableTidilyInPolyTime list input (encList encUnary))
     (hpos : ∀ a, ∀ p ∈ list a, 0 < p) {B : α → ℕ}
     (hB : PolyBounded (fun a => (input a).length) B) (hle : ∀ a, (list a).prod ≤ B a) :
@@ -202,7 +203,7 @@ theorem computableTidilyInPolyTime_primesIoc :
 def selectStep (state : ℕ × List ℕ) (p : ℕ) : ℕ × List ℕ :=
   if p ≤ state.1 then (state.1 / p, state.2 ++ [p]) else state
 
-theorem foldl_selectStep (T : ℕ) (ps chosen : List ℕ) :
+private theorem foldl_selectStep (T : ℕ) (ps chosen : List ℕ) :
     (ps.foldl selectStep (T, chosen)).2 = chosen ++ selectBelow T ps := by
   induction ps generalizing T chosen with
   | nil => simp [selectBelow]
@@ -255,14 +256,14 @@ theorem computableTidilyInPolyTime_degreePrimes :
   unfold degreePrimes
   fun_prop
 
-theorem selectBelow_zero {ps : List ℕ} (hps : ∀ p ∈ ps, 0 < p) : selectBelow 0 ps = [] := by
+private theorem selectBelow_zero {ps : List ℕ} (hps : ∀ p ∈ ps, 0 < p) : selectBelow 0 ps = [] := by
   induction ps with
   | nil => rfl
   | cons p ps ih =>
     rw [selectBelow, ite_eq_right_iff.2 (by have := hps p List.mem_cons_self; omega)]
     exact ih fun q hq => hps q (List.mem_cons_of_mem _ hq)
 
-theorem prod_degreePrimes_le (N : ℕ) : (degreePrimes N).prod ≤ N + 1 := by
+private theorem prod_degreePrimes_le (N : ℕ) : (degreePrimes N).prod ≤ N + 1 := by
   rcases Nat.eq_zero_or_pos (N / (Nat.log 2 N + 1) ^ 2) with hT | hT
   · rw [degreePrimes, hT, selectBelow_zero fun p hp => (mem_primesIoc.1 hp).2.2.pos]
     simp
@@ -328,7 +329,7 @@ theorem computableTidilyInPolyTime_explicitPowerTables :
 
 /-- The mixed-radix digits in the radix of the field degree on `N` bits; every partial product of
 the radix is at most `N + 1`. -/
-theorem computableTidilyInPolyTime_mixedDigit_degreePrimes :
+private theorem computableTidilyInPolyTime_mixedDigit_degreePrimes :
     ComputableTidilyInPolyTime (fun q : (ℕ × ℕ) × ℕ => mixedDigit (degreePrimes q.1.1) q.1.2 q.2)
       (encPair (encPair encUnary encUnary) encUnary) encUnary := by
   have htake : ComputableTidilyInPolyTime (fun q : (ℕ × ℕ) × ℕ => (degreePrimes q.1.1).take q.2)
@@ -358,7 +359,7 @@ theorem computableTidilyInPolyTime_mixedDigit_degreePrimes' {α : Type} {input :
 
 
 /-- Coordinates of the products of monomials of the explicit field on `N` bits, `N` in unary. -/
-theorem computableTidilyInPolyTime_monomialBit_explicit : ComputableTidilyInPolyTime
+private theorem computableTidilyInPolyTime_monomialBit_explicit : ComputableTidilyInPolyTime
     (fun q : ((ℕ × ℕ) × ℕ) × ℕ =>
       monomialBit (degreePrimes q.1.1.1) (explicitPowerTables q.1.1.1) q.1.1.2 q.1.2 q.2)
     (encPair (encPair (encPair encUnary encUnary) encUnary) encUnary) encBool := by
@@ -426,7 +427,7 @@ theorem length_fieldMul (tab : List (List (List Bool))) (a b : List Bool) :
 
 /-- The powers `y ^ (2 ^ (k + 1) - 1)`, by `k` multiplications and squarings; every
 intermediate power has `n` coordinates. -/
-theorem computableTidilyInPolyTime_powerPred : ComputableTidilyInPolyTime
+private theorem computableTidilyInPolyTime_powerPred : ComputableTidilyInPolyTime
     (fun p : List (List (List Bool)) × List Bool × ℕ => powerPred p.1 p.2.1 p.2.2)
     (encPair encTable (encPair encBits encUnary)) encBits := by
   unfold powerPred
@@ -446,20 +447,20 @@ theorem computableTidilyInPolyTime_powerPred' {α : Type} {input : α ↪ List B
     computableTidilyInPolyTime_powerPred.comp (htab.prod (hy.prod hk))
 
 /-- One step of the dynamic program for the elementary symmetric polynomials. -/
-theorem computableTidilyInPolyTime_esymmStep : ComputableTidilyInPolyTime
+private theorem computableTidilyInPolyTime_esymmStep : ComputableTidilyInPolyTime
     (fun p : (List (List (List Bool)) × List (List Bool)) × List Bool =>
       esymmStep p.1.1 p.1.2 p.2)
     (encPair (encPair encTable (encList encBits)) encBits) (encList encBits) := by
   unfold esymmStep
   fun_prop
 
-theorem length_esymmStep (tab : List (List (List Bool))) (E : List (List Bool))
+private theorem length_esymmStep (tab : List (List (List Bool))) (E : List (List Bool))
     (z : List Bool) : (esymmStep tab E z).length = E.length := by
   simp [esymmStep]
 
 /-- **The elementary symmetric polynomial `e_t` in coordinates**: the dynamic program keeps `t`
 words of at most `n` coordinates. -/
-theorem computableTidilyInPolyTime_esymmCoords : ComputableTidilyInPolyTime
+private theorem computableTidilyInPolyTime_esymmCoords : ComputableTidilyInPolyTime
     (fun p : (List (List (List Bool)) × ℕ) × List (List Bool) => esymmCoords p.1.1 p.1.2 p.2)
     (encPair (encPair encTable encUnary) (encList encBits)) encBits := by
   have hsize : ComputableTidilyInPolyTime
@@ -503,7 +504,7 @@ theorem computableTidilyInPolyTime_esymmCoords' {α : Type} {input : α ↪ List
     computableTidilyInPolyTime_esymmCoords.comp ((htab.prod ht).prod hzs)
 
 /-- The traces of the basis elements, from the diagonals of the multiplication table. -/
-theorem computableTidilyInPolyTime_traceVector :
+private theorem computableTidilyInPolyTime_traceVector :
     ComputableTidilyInPolyTime traceVector encTable encBits := by
   unfold traceVector
   fun_prop
@@ -516,7 +517,7 @@ theorem computableTidilyInPolyTime_traceVector' {α : Type} {input : α ↪ List
   simpa only [Function.comp_def] using computableTidilyInPolyTime_traceVector.comp htab
 
 /-- The trace as a bit. -/
-theorem computableTidilyInPolyTime_traceBit : ComputableTidilyInPolyTime
+private theorem computableTidilyInPolyTime_traceBit : ComputableTidilyInPolyTime
     (fun p : List Bool × List Bool => traceBit p.1 p.2) (encPair encBits encBits) encBool := by
   unfold traceBit
   fun_prop
@@ -541,7 +542,7 @@ theorem computableTidilyInPolyTime_traceSymCoords : ComputableTidilyInPolyTime
 /-! ### The explicit disperser -/
 
 /-- **The program is polynomial-time.** -/
-theorem computableTidilyInPolyTime_explicitDisperserProgram :
+private theorem computableTidilyInPolyTime_explicitDisperserProgram :
     ComputableTidilyInPolyTime explicitDisperserProgram encBits encBool := by
   unfold explicitDisperserProgram
   simpa only [Function.comp_def] using computableTidilyInPolyTime_traceSymCoords.comp

Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean

@@ -123,7 +123,8 @@ theorem computableTidilyInPolyTime_merlinArthurRepeat {V : α × List Bool → B
 
 /-- On a proof followed by `2 r(n)` rows of `p(n)` bits, the majority vote compares the number of
 rows accepted with the proof with `r(n)`. -/
-theorem merlinArthurRepeat_ofFn_append_ofFn {q r p : Polynomial ℕ} {V : α × List Bool → Bool}
+private theorem merlinArthurRepeat_ofFn_append_ofFn {q r p : Polynomial ℕ}
+    {V : α × List Bool → Bool}
     (a : α) (y : Fin (q.eval (enc a).length) → Bool)
     (x : BitString (2 * r.eval (enc a).length * p.eval (enc a).length)) :
     merlinArthurRepeat enc q r p V (a, List.ofFn y ++ List.ofFn x) = decide (r.eval (enc a).length <
@@ -235,7 +236,8 @@ theorem computableTidilyInPolyTime_arthurMerlinRepeat {V : α × List Bool → B
 
 /-- On `2 r(n)` rows followed by `2 r(n)` replies, the parallel majority vote compares the number
 of rows accepted with their replies with `r(n)`. -/
-theorem arthurMerlinRepeat_ofFn_append_ofFn {r p q : Polynomial ℕ} {V : α × List Bool → Bool}
+private theorem arthurMerlinRepeat_ofFn_append_ofFn {r p q : Polynomial ℕ}
+    {V : α × List Bool → Bool}
     (a : α) (x : BitString (2 * r.eval (enc a).length * p.eval (enc a).length))
     (y : BitString (2 * r.eval (enc a).length * q.eval (enc a).length)) :
     arthurMerlinRepeat enc r p q V (a, List.ofFn x ++ List.ofFn y) =

Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean

@@ -85,12 +85,12 @@ namespace PublicCoin
 variable {n : ℕ}
 
 /-- Relabelling by a product of permutations is relabelling twice. -/
-theorem reindex_mul (σ τ : Equiv.Perm (Fin n)) (M : Matrix (Fin n) (Fin n) Bool) :
+private theorem reindex_mul (σ τ : Equiv.Perm (Fin n)) (M : Matrix (Fin n) (Fin n) Bool) :
     Matrix.reindex (σ * τ) (σ * τ) M = Matrix.reindex σ σ (Matrix.reindex τ τ M) :=
   (DFunLike.congr_fun (Matrix.reindex_trans τ τ σ σ) M).symm
 
 /-- Relabelling by the identity permutation does nothing. -/
-theorem reindex_one (M : Matrix (Fin n) (Fin n) Bool) : Matrix.reindex 1 1 M = M :=
+private theorem reindex_one (M : Matrix (Fin n) (Fin n) Bool) : Matrix.reindex 1 1 M = M :=
   Matrix.reindex_refl_refl M
 
 /-- `Matrix.reindex τ τ A = M` says that `τ` carries `A` to `M`. -/
@@ -107,7 +107,7 @@ theorem reindex_eq_iff {τ : Equiv.Perm (Fin n)} {A M : Matrix (Fin n) (Fin n) B
 def orbit (A : Matrix (Fin n) (Fin n) Bool) : Finset (Matrix (Fin n) (Fin n) Bool) :=
   univ.image fun τ => Matrix.reindex τ τ A
 
-theorem mem_orbit {A M : Matrix (Fin n) (Fin n) Bool} :
+private theorem mem_orbit {A M : Matrix (Fin n) (Fin n) Bool} :
     M ∈ orbit A ↔ ∃ τ, Matrix.reindex τ τ A = M := by
   simp [orbit]
 
@@ -129,7 +129,7 @@ def pairs (A : Matrix (Fin n) (Fin n) Bool) :
 
 /-- A relabelling `M` of `A` has as many automorphisms as there are permutations carrying `A` to
 `M`: composing with one permutation carrying `A` to `M` is a bijection. -/
-theorem card_filter_reindex_eq {A M : Matrix (Fin n) (Fin n) Bool} (hM : M ∈ orbit A) :
+private theorem card_filter_reindex_eq {A M : Matrix (Fin n) (Fin n) Bool} (hM : M ∈ orbit A) :
     #{σ : Equiv.Perm (Fin n) | Matrix.reindex σ σ M = M} =
       #{τ : Equiv.Perm (Fin n) | Matrix.reindex τ τ A = M} := by
   obtain ⟨τ₀, rfl⟩ := mem_orbit.1 hM
@@ -189,14 +189,14 @@ private theorem index_symm {q : ℕ} (h : q < n * n) :
 def matrixBit (A : Matrix (Fin n) (Fin n) Bool) (q : ℕ) : Bool :=
   if h : q < n * n then BitString.blocksEquiv.symm (Matrix.of.symm A) ⟨q, h⟩ else false
 
-theorem matrixBit_index (A : Matrix (Fin n) (Fin n) Bool) (i j : Fin n) :
+private theorem matrixBit_index (A : Matrix (Fin n) (Fin n) Bool) (i j : Fin n) :
     matrixBit A (i * n + j) = A i j := by
   have hq : (⟨i * n + j, index_lt i j⟩ : Fin (n * n)) = finProdFinEquiv (i, j) :=
     Fin.ext (val_finProdFinEquiv i j).symm
   simp only [matrixBit, index_lt i j, ↓reduceDIte, hq, BitString.blocksEquiv_symm_apply,
     Matrix.of_symm_apply, Equiv.symm_apply_apply]
 
-theorem matrixBit_of_le (A : Matrix (Fin n) (Fin n) Bool) {q : ℕ} (h : n * n ≤ q) :
+private theorem matrixBit_of_le (A : Matrix (Fin n) (Fin n) Bool) {q : ℕ} (h : n * n ≤ q) :
     matrixBit A q = false := by
   simp [matrixBit, Nat.not_lt.2 h]
 
@@ -214,27 +214,27 @@ def code (E : ℕ) (M : Matrix (Fin n) (Fin n) Bool) (σ : Equiv.Perm (Fin n)) :
 
 /-- Bit `q` of a certificate naming the graph `b` and a permutation `τ`: `b`, then the entries of
 the matrix of `τ`, row by row, then `false`. -/
-def certBit (b : Bool) (τ : Equiv.Perm (Fin n)) (q : ℕ) : Bool :=
+private def certBit (b : Bool) (τ : Equiv.Perm (Fin n)) (q : ℕ) : Bool :=
   if q = 0 then b else matrixBit (Matrix.of fun i j => decide (τ i = j)) (q - 1)
 
 /-- A certificate naming the graph `b` and a permutation `τ`, in `C` bits. -/
-def cert (C : ℕ) (b : Bool) (τ : Equiv.Perm (Fin n)) : BitString C :=
+private def cert (C : ℕ) (b : Bool) (τ : Equiv.Perm (Fin n)) : BitString C :=
   fun q => certBit b τ q
 
 private theorem getD_ofFn {E : ℕ} (x : BitString E) {p : ℕ} (hp : p < E) :
     (List.ofFn x).getD p false = x ⟨p, hp⟩ := by
   rw [List.getD_eq_getElem _ _ (by simpa using hp), List.getElem_ofFn]
 
 /-- The matrix read from the first `n * n` bits of a word. -/
-def decodeMatrix (n : ℕ) (u : List Bool) : Matrix (Fin n) (Fin n) Bool :=
+private def decodeMatrix (n : ℕ) (u : List Bool) : Matrix (Fin n) (Fin n) Bool :=
   Matrix.of fun i j => u.getD (i * n + j) false
 
 /-- The map read from the matrix starting after `k` bits of a word: row `i` selects its first set
 bit (`Cslib.Complexity.GraphIsomorphism.image`). -/
-def decodeMap (n k : ℕ) (u : List Bool) (i : Fin n) : Fin n :=
+private def decodeMap (n k : ℕ) (u : List Bool) (i : Fin n) : Fin n :=
   ⟨GraphIsomorphism.image n (u.drop k) i, GraphIsomorphism.image_lt _ _ i.pos⟩
 
-theorem decodeMatrix_code {E : ℕ} (hE : n * n ≤ E) (M : Matrix (Fin n) (Fin n) Bool)
+private theorem decodeMatrix_code {E : ℕ} (hE : n * n ≤ E) (M : Matrix (Fin n) (Fin n) Bool)
     (σ : Equiv.Perm (Fin n)) : decodeMatrix n (List.ofFn (code E M σ)) = M := by
   ext i j
   rw [decodeMatrix, Matrix.of_apply, getD_ofFn _ ((index_lt i j).trans_le hE)]
@@ -245,7 +245,7 @@ private theorem decide_val_eq {σ : Equiv.Perm (Fin n)} {i : Fin n} {j : ℕ} (h
     decide (σ i = ⟨j, hj⟩) = decide (j = σ i) :=
   decide_eq_decide.2 ⟨fun h => by rw [h], fun h => Fin.ext h.symm⟩
 
-theorem decodeMap_code {E : ℕ} (hE : 2 * (n * n) ≤ E) (M : Matrix (Fin n) (Fin n) Bool)
+private theorem decodeMap_code {E : ℕ} (hE : 2 * (n * n) ≤ E) (M : Matrix (Fin n) (Fin n) Bool)
     (σ : Equiv.Perm (Fin n)) : decodeMap n (n * n) (List.ofFn (code E M σ)) = σ := by
   funext i
   refine Fin.ext (GraphIsomorphism.image_eq (σ i).2 fun j hj => ?_)
@@ -256,12 +256,12 @@ theorem decodeMap_code {E : ℕ} (hE : 2 * (n * n) ≤ E) (M : Matrix (Fin n) (F
     Nat.add_sub_cancel_left]
   rw [matrixBit_index _ i ⟨j, hj⟩, Matrix.of_apply, decide_val_eq hj]
 
-theorem getD_ofFn_cert_zero {C : ℕ} (hC : 0 < C) (b : Bool) (τ : Equiv.Perm (Fin n)) :
+private theorem getD_ofFn_cert_zero {C : ℕ} (hC : 0 < C) (b : Bool) (τ : Equiv.Perm (Fin n)) :
     (List.ofFn (cert C b τ)).getD 0 false = b := by
   rw [getD_ofFn _ hC]
   simp [cert, certBit]
 
-theorem decodeMap_cert {C : ℕ} (hC : n * n + 1 ≤ C) (b : Bool) (τ : Equiv.Perm (Fin n)) :
+private theorem decodeMap_cert {C : ℕ} (hC : n * n + 1 ≤ C) (b : Bool) (τ : Equiv.Perm (Fin n)) :
     decodeMap n 1 (List.ofFn (cert C b τ)) = τ := by
   funext i
   refine Fin.ext (GraphIsomorphism.image_eq (τ i).2 fun j hj => ?_)
@@ -332,22 +332,22 @@ section Check
 
 variable {E : ℕ} {adj : Bool → ℕ → ℕ → Bool} {u v : List Bool}
 
-theorem injective_decodeMap_left (h : check n E adj u v = true) :
+private theorem injective_decodeMap_left (h : check n E adj u v = true) :
     Function.Injective (decodeMap n (n * n) u) := by
   intro i j hij
   rcases ((check_eq_true_iff.1 h).2 i i.2 j j.2).2.1 with h' | h'
   · exact Fin.ext h'
   · exact absurd (congrArg Fin.val hij) h'
 
-theorem injective_decodeMap_right (h : check n E adj u v = true) :
+private theorem injective_decodeMap_right (h : check n E adj u v = true) :
     Function.Injective (decodeMap n 1 v) := by
   intro i j hij
   rcases ((check_eq_true_iff.1 h).2 i i.2 j j.2).2.2.2.1 with h' | h'
   · exact Fin.ext h'
   · exact absurd (congrArg Fin.val hij) h'
 
 /-- The map selected by an accepted element is an automorphism of its matrix. -/
-theorem reindex_decodeMatrix (h : check n E adj u v = true) :
+private theorem reindex_decodeMatrix (h : check n E adj u v = true) :
     Matrix.reindex
         (Equiv.ofBijective _ (Finite.injective_iff_bijective.1 (injective_decodeMap_left h)))
         (Equiv.ofBijective _ (Finite.injective_iff_bijective.1 (injective_decodeMap_left h)))
@@ -356,7 +356,7 @@ theorem reindex_decodeMatrix (h : check n E adj u v = true) :
   reindex_eq_iff.2 fun i j => ((check_eq_true_iff.1 h).2 i i.2 j j.2).2.2.1
 
 /-- The matrix of an accepted element is a relabelling of the graph named by the certificate. -/
-theorem decodeMatrix_mem_orbit (h : check n E adj u v = true) :
+private theorem decodeMatrix_mem_orbit (h : check n E adj u v = true) :
     decodeMatrix n u ∈ orbit (Matrix.of fun i j : Fin n => adj (v.getD 0 false) i j) :=
   mem_orbit.2
     ⟨Equiv.ofBijective _ (Finite.injective_iff_bijective.1 (injective_decodeMap_right h)),

Complexity/Computability/Complexity/Classes/Hierarchy.lean

@@ -192,7 +192,7 @@ theorem computableTidilyInO_verdict :
 /-- The numeric core of the resources of the diagonal: for an input of length `n`, a decoded
 description of encoded length `D`, encoded symbols of length `N`, a clock `J ≥ 1` and a result of
 encoded length `E`, everything is within `K * M ^ 5 * J ^ 3` steps and `K * M ^ 5 * J` cells. -/
-theorem bounds_aux {n A D N J L I E cD cO M K : ℕ} (hJ : 1 ≤ J)
+private theorem bounds_aux {n A D N J L I E cD cO M K : ℕ} (hJ : 1 ≤ J)
     (hD : D ≤ cD * (A + 1)) (hN : N ≤ 3 * n) (hL : L = n + 1) (hI : I = 2 * D + 1 + (2 * N + 1 + L))
     (hM : M = cD * (A + 1) + A + 4 * n + 2) (hK : K = 100100 + 44100 * (cO + 1) ^ 2)
     (hE : E ≤ cO * (A + (n + n) + (runBound D N J + I) + 1)) :

Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean

@@ -87,15 +87,15 @@ open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Universal Filter
 namespace Diagonal
 
 /-- The space of the universal run grows with the number of steps. -/
-theorem runBound_le_succ (D N J : ℕ) : runBound D N J ≤ runBound D N (J + 1) := by
+private theorem runBound_le_succ (D N J : ℕ) : runBound D N J ≤ runBound D N (J + 1) := by
   simp only [runBound, ctxBound, cfgBound, tapeBound]
   gcongr <;> omega
 
 /-- The numeric core of the resources of the clocked diagonal: for an input of length `n`, a
 decoding time `A` linear in `n`, a decoded description of encoded length `D`, encoded symbols of
 length `N`, a clock `J` of `L` binary digits and a result of encoded length `E`, everything is
 within `K * (n + 1) ^ 5 * (J + 1) ^ 3` steps and cells. -/
-theorem clockedBounds_aux (cA cD cO C₂ : ℕ) : ∃ K, ∀ {n A D N J L I E : ℕ},
+private theorem clockedBounds_aux (cA cD cO C₂ : ℕ) : ∃ K, ∀ {n A D N J L I E : ℕ},
     A ≤ cA * (n + 1) → D ≤ cD * (n + A + 1) → N ≤ 3 * n → (L + 1) ^ 2 ≤ C₂ * (J + 1) →
     I = 2 * D + 1 + (2 * N + 1 + L) →
     E ≤ cO * (n + A + (n + J) + (runBound D N J + I) + 1) →