style improvements

Complexitylib/Circuits/AC0/Iteration/Internal.lean

@@ -25,16 +25,12 @@ namespace Switching
 
 attribute [local instance] Classical.propDecidable
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private def finiteEventCount {α : Type} [Fintype α]
-    [DecidableEq α] (event : α → Prop)
+private def finiteEventCount {α : Type} [Fintype α] (event : α → Prop)
     [DecidablePred event] : ℕ :=
   (Finset.univ.filter event).card
 
 private theorem finiteEventCount_mono
-    {α : Type} [Fintype α] [DecidableEq α]
+    {α : Type} [Fintype α]
     (left right : α → Prop)
     [DecidablePred left] [DecidablePred right]
     (himp : ∀ value, left value → right value) :
@@ -62,7 +58,6 @@ private theorem finiteEventCount_or_le_add
 
 private theorem finiteEventCount_prod
     {α β : Type} [Fintype α] [Fintype β]
-    [DecidableEq α] [DecidableEq β]
     (event : α → β → Prop)
     [∀ first, DecidablePred (event first)] :
     finiteEventCount
@@ -89,7 +84,6 @@ private theorem finiteEventCount_prod
 
 private theorem finiteEventCount_prod_mul_le
     {α β : Type} [Fintype α] [Fintype β]
-    [DecidableEq α] [DecidableEq β]
     (event : α → β → Prop)
     [∀ first, DecidablePred (event first)]
     (multiplier bound : ℕ)
@@ -110,7 +104,6 @@ private theorem finiteEventCount_prod_mul_le
 
 private theorem finiteEventCount_prod_left
     {α β : Type} [Fintype α] [Fintype β]
-    [DecidableEq α] [DecidableEq β]
     (event : α → Prop) [DecidablePred event] :
     finiteEventCount
         (fun pair : α × β => event pair.1) =
@@ -133,12 +126,8 @@ private theorem finiteEventCount_prod_left
     _ = finiteEventCount event * Fintype.card β := by
           simp [finiteEventCount]
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
 private theorem finiteEventCount_exists_mem_le_sum
-    {α β : Type} [Fintype α] [DecidableEq α]
-    [DecidableEq β] (values : List β)
+    {α β : Type} [Fintype α] (values : List β)
     (event : β → α → Prop)
     [∀ value, DecidablePred (event value)] :
     finiteEventCount (fun sample =>
@@ -170,7 +159,7 @@ private theorem finiteEventCount_exists_mem_le_sum
           simp
 
 private theorem exists_not_event_of_weight_sum
-    {α : Type} [Fintype α] [DecidableEq α]
+    {α : Type} [Fintype α]
     (event : α → Prop) [DecidablePred event]
     (weight : α → ℕ) (cap threshold : ℕ)
     (hcap : ∀ value, weight value ≤ cap)

Complexitylib/Circuits/Basic.lean

@@ -207,9 +207,6 @@ Primary input vertices are not counted, and the negation flags on gate inputs
 have zero cost. Some texts instead count input vertices and explicit NOT gates;
 those conventions agree only up to additive/linear overhead, not on exact size
 bounds. -/
--- The circuit argument is unused by design: `size` is determined by the
--- indices, and the argument exists purely to enable `c.size` dot notation.
-@[nolint unusedArguments]
 def size (_ : Circuit B N M G) : Nat := G + M
 
 end Circuit
@@ -258,16 +255,14 @@ noncomputable def sizeComplexityWithTop
     (B : Basis) (f : BitString N → Bool) : WithTop Nat :=
   sInf ((fun s : Nat => (s : WithTop Nat)) '' realizationSizes B f)
 
-/-- The minimum circuit size over a complete basis `B` computing `f`.
+/-- The minimum circuit size over a basis `B` computing `f`.
 
-This natural-valued interface requires completeness so that the set of
-realizing circuits is nonempty. Use `sizeComplexityWithTop` when the basis may
-be incomplete. -/
--- Completeness is an intentional API precondition. The infimum expression
--- itself does not inspect the selected witness.
-@[nolint unusedArguments]
+The results that identify this with an achieved size take `[CompleteBasis B]`,
+which makes the set of realizing circuits nonempty. Over an incomplete basis
+the infimum of the empty set is `0`, so an unrealizable function would be
+indistinguishable from a zero-size one; use `sizeComplexityWithTop` there. -/
 noncomputable def sizeComplexity
-    (B : Basis) [CompleteBasis B] (f : BitString N → Bool) : Nat :=
+    (B : Basis) (f : BitString N → Bool) : Nat :=
   sInf (realizationSizes B f)
 
 private theorem realizationSizes_nonempty [CompleteBasis B]
@@ -350,7 +345,7 @@ theorem sizeComplexity_pos [CompleteBasis B]
   omega
 
 /-- Any circuit computing `f` has size at least `sizeComplexity B f`. -/
-theorem sizeComplexity_le [CompleteBasis B] {G : Nat}
+theorem sizeComplexity_le {G : Nat}
     (c : Circuit B N 1 G) (f : BitString N → Bool)
     (hf : (fun x => (c.eval x) 0) = f) :
     sizeComplexity B f ≤ c.size :=

Complexitylib/Circuits/Encoding/Machine/Core/Defs.lean

@@ -380,7 +380,6 @@ def FamilyCorePre (codeBits inputBits : List Bool) (initialInput : Tape)
 core. Malformed codes and successful false evaluations both write zero. The
 terminal work tapes are intentionally unconstrained because rejecting parses
 halt at different code, memo, and counter cursor positions. -/
-@[nolint unusedArguments]
 def FamilyCorePost (codeBits inputBits : List Bool) (initialInput : Tape)
     (inp : Tape) (_work : Fin workTapeCount → Tape) (out : Tape) : Prop :=
   inp = initialInput ∧
@@ -402,7 +401,6 @@ def evalFamilyTime (n : ℕ) : ℕ :=
 cells retain the original encoding and the output carries the defaulted paired
 evaluation verdict with its canonical head and left-marker invariant. Terminal
 work tapes are intentionally unconstrained across valid and rejecting branches. -/
-@[nolint unusedArguments]
 def EvalFamilyPost (bits : List Bool) (inp : Tape)
     (_work : Fin workTapeCount → Tape) (out : Tape) : Prop :=
   inp.cells = (Tape.init (bits.map Γ.ofBool)).cells ∧

Complexitylib/Circuits/Family.lean

@@ -58,7 +58,7 @@ theorem Computes.sizeComplexityWithTop_le {c : Circuit B N 1 G}
 
 /-- Over a complete basis, any circuit computing `f` witnesses a natural-valued
 upper bound on its size complexity. -/
-theorem Computes.sizeComplexity_le [CompleteBasis B] {c : Circuit B N 1 G}
+theorem Computes.sizeComplexity_le {c : Circuit B N 1 G}
     {f : BitString N → Bool} (h : c.Computes f) :
     sizeComplexity B f ≤ c.size :=
   Circuit.sizeComplexity_le c f h

Complexitylib/Circuits/Internal/ShannonUpper.lean

@@ -657,10 +657,6 @@ theorem encodeColumn_lt (k : Nat) (col : Fin (2^k) → Bool) :
 /-- The column function of `f` at data row `y`: maps an address `a` to
     `f(a, y)`, reading the first `k` input bits from `a` and the remaining
     `q` bits from `y`. -/
--- `_hkq : k + q = N` is a documented precondition tying the address width
--- `k` and data width `q` to `N`; it is threaded by every caller but not
--- needed in the body, which is polymorphic in `k`, `q`.
-@[nolint unusedArguments]
 noncomputable def columnFunction (N : Nat) (f : BitString N → Bool)
     (k q : Nat) (_hkq : k + q = N) (y : Fin (2^q)) : Fin (2^k) → Bool :=
   fun a => f (fun idx =>
@@ -681,10 +677,7 @@ theorem columnPatternIndex_lt (N : Nat) (f : BitString N → Bool)
 
 /-! ### Shannon gate array -/
 
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private noncomputable def shannonGateArray (N : Nat) [NeZero N]
+private noncomputable def shannonGateArray (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) :
     (i : Fin (totalSectionGates (addrBits N) (dataBits N))) →
     { g : Gate Basis.andOr2 (N + totalSectionGates (addrBits N) (dataBits N)) //
@@ -1021,10 +1014,7 @@ private def shiftedBits (N k q : Nat) (hkq : k + q = N) (x : BitString N) :
   fun j => x ⟨k + j.val, by have := j.isLt; omega⟩
 
 /-- columnFunction at the actual bit-vector address/data values equals f(x). -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private theorem columnFunction_at_actual_bits (N : Nat) [NeZero N]
+private theorem columnFunction_at_actual_bits (N : Nat)
     (f : BitString N → Bool) (x : BitString N)
     (k q : Nat) (hkq : k + q = N) :
     let addr : BitString k := fun j => x ⟨j.val, by have := j.isLt; omega⟩
@@ -1130,25 +1120,22 @@ private theorem dataSum_lt (N : Nat) (hN : 16 ≤ N) (x : BitString N) :
   sum_cond_pow_fin_lt (dataBits N) (shiftedBits N (addrBits N) (dataBits N) (addrDataSum N hN) x)
 
 /-- andLayerSem at y is false when y ≠ dataSum. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private theorem andLayerSem_ne (N : Nat) [NeZero N]
+private theorem andLayerSem_ne (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) (x : BitString N)
     (y : Nat) (hy : y < 2 ^ dataBits N) (hne : y ≠ dataSum N hN x) :
     andLayerSem N f hN x y hy = false := by
   unfold andLayerSem dataSum at *
   simp only [beq_eq_false_iff_ne.mpr hne, Bool.false_and]
 
 /-- andLayerSem at dataSum gives columnFunction at actual bits. -/
-private theorem andLayerSem_eq (N : Nat) [NeZero N]
+private theorem andLayerSem_eq (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) (x : BitString N) :
     andLayerSem N f hN x (dataSum N hN x) (dataSum_lt N hN x) = f x := by
   unfold andLayerSem dataSum
   simp only [beq_self_eq_true, Bool.true_and]
   exact columnFunction_at_actual_bits N f x (addrBits N) (dataBits N) (addrDataSum N hN)
 
-private theorem or_andLayerSem_eq_f (N : Nat) [NeZero N]
+private theorem or_andLayerSem_eq_f (N : Nat)
     (f : BitString N → Bool) (hN : 16 ≤ N) (x : BitString N) :
     (List.range (2 ^ dataBits N)).foldl
       (fun acc y => acc || if h : y < 2 ^ dataBits N

Complexitylib/Circuits/Internal/Valiant.lean

@@ -156,10 +156,7 @@ omit [Fintype V] in
 /-- **Extending a simple path by an edge.** In an acyclic digraph, a
 simple path `p` ending at `u` followed by an edge `u → v` yields a
 simple path ending at `v` that is one longer. -/
--- The signature mirrors the family this belongs to; the argument is part of
--- that shape even where this member does not consult it.
-@[nolint unusedArguments]
-private lemma extend_simple_path [DecidableEq V] (G : Digraph V) (hac : IsAcyclic G)
+private lemma extend_simple_path (G : Digraph V) (hac : IsAcyclic G)
     {u v : V} (huv : G.Adj u v) {n : ℕ} {p : Fin (n + 1) → V}
     (hsp : G.IsPath p) (hpu : p (Fin.last n) = u) :
     ∃ p' : Fin (n + 2) → V, G.IsPath p' ∧ p' (Fin.last (n + 1)) = v := by
@@ -190,7 +187,7 @@ private lemma extend_simple_path [DecidableEq V] (G : Digraph V) (hac : IsAcycli
 ending at `u` followed by the edge `(u,v)` is a strictly longer simple
 path ending at `v` (using acyclicity to ensure `v` does not already
 appear in the path). -/
-lemma canonicalLabel_isLegal [DecidableEq V] (G : Digraph V) (hac : IsAcyclic G) :
+lemma canonicalLabel_isLegal (G : Digraph V) (hac : IsAcyclic G) :
     IsLegalLabeling G G.canonicalLabel := by
   intro u v huv
   obtain ⟨p, hsp, hpu⟩ :=
@@ -362,6 +359,7 @@ noncomputable def levelEdges
   G.edgeFinset.filter (fun e =>
     firstDifferBit k (G.canonicalLabel e.1 - 1) (G.canonicalLabel e.2 - 1) = i)
 
+omit [DecidableEq V] in
 /-- For any edge `(u,v)` of an acyclic `G` with `depth ≤ 2 ^ k`, the first
 MSB-disagreement of the `k`-bit canonical labels is in `{1,...,k}`. -/
 private lemma firstDifferBit_mem_Ioc
@@ -380,6 +378,7 @@ private lemma firstDifferBit_mem_Ioc
     (canonicalLabel_sub_one_lt_two_pow G hd _)
   exact Finset.mem_Ioc.mpr ⟨hpos, hle⟩
 
+omit [DecidableEq V] in
 /-- **Partition.** When `G` is acyclic and `G.depth ≤ 2 ^ k`, every
 edge lies in exactly one level `E_i` for `i ∈ {1,...,k}`. -/
 lemma sum_card_levelEdges_eq
@@ -435,6 +434,7 @@ private lemma exists_r_subset_sum_le
       have hih_step : n' * (∑ i ∈ I, a i) ≤ r * (∑ i ∈ s', a i) := hI_le
       omega
 
+omit [DecidableEq V] in
 /-- **Averaging.** There is a choice of `r` levels whose total edge
 count is at most `r * S / k` (equivalently, `k * total ≤ r * S`). -/
 lemma exists_r_levels_small

Complexitylib/Circuits/Nondeterminism.lean

@@ -106,7 +106,7 @@ theorem sizeComplexity_or_le [CompleteBasis Basis.andOr2] [NeZero N]
 
 /-- Circuit complexity is invariant under propositional equality of input
     dimension. -/
-private theorem sizeComplexity_cast [CompleteBasis B] [NeZero n] [NeZero n']
+private theorem sizeComplexity_cast [NeZero n] [NeZero n']
     (h : n = n') (f : BitString n → Bool) :
     Circuit.sizeComplexity B (h ▸ f : BitString n' → Bool) =
       Circuit.sizeComplexity B f := by
@@ -200,7 +200,7 @@ theorem sizeComplexity_existsQuantify_le [CompleteBasis Basis.andOr2]
     exponential circuit complexity,
     `existsQuantify f` has complexity at most `O(2^m / m)`, which decreases
     exponentially as more variables are quantified away. -/
-theorem sizeComplexity_existsQuantify_le_shannon [CompleteBasis Basis.andOr2]
+theorem sizeComplexity_existsQuantify_le_shannon
     (f : BitString (k + m) → Bool) [NeZero m] (hm : 16 ≤ m) :
     Circuit.sizeComplexity Basis.andOr2 (existsQuantify f) ≤ 18 * 2 ^ m / m :=
   shannon_upper_bound m hm (existsQuantify f)

Complexitylib/Circuits/NormalForm/Defs.lean

@@ -49,8 +49,6 @@ structure Literal (N : Nat) where
   polarity : Bool
   deriving Repr, DecidableEq
 
--- These record printers intentionally ignore precedence.
-attribute [nolint unusedArguments] instReprLiteral.repr
 
 /-- Evaluate a literal on a bit assignment. -/
 def Literal.eval (l : Literal N) (x : BitString N) : Bool :=
@@ -118,8 +116,6 @@ structure CNF (N : Nat) where
   clauses : List (List (Literal N))
   deriving Repr, DecidableEq
 
--- These record printers intentionally ignore precedence.
-attribute [nolint unusedArguments] instReprCNF.repr
 
 namespace CNF
 
@@ -212,8 +208,6 @@ structure DNF (N : Nat) where
   terms : List (List (Literal N))
   deriving Repr, DecidableEq
 
--- These record printers intentionally ignore precedence.
-attribute [nolint unusedArguments] instReprDNF.repr
 
 namespace DNF
 

Complexitylib/Circuits/Shannon.lean

@@ -79,8 +79,7 @@ theorem shannon_sizeComplexity (N : Nat) [NeZero N] (hN : 6 ≤ N)
     This is the full-column-library variant (C = 18). The tighter
     `(1 + o(1)) · 2^N / N` bound due to Lupanov (1958) uses column
     grouping and is not yet formalized. -/
-theorem shannon_upper_bound [CompleteBasis Basis.andOr2]
-    (N : Nat) (hN : 16 ≤ N) [NeZero N]
+theorem shannon_upper_bound (N : Nat) (hN : 16 ≤ N) [NeZero N]
     (f : BitString N → Bool) :
     Circuit.sizeComplexity Basis.andOr2 f ≤ 18 * 2 ^ N / N := by
   obtain ⟨G, c, heval, hsize⟩ := ShannonUpper.shannon_construction N hN f

Complexitylib/Circuits/Threshold/Defs.lean

@@ -29,8 +29,6 @@ structure ThresholdOp where
   cutoff : ℕ
   deriving Repr, DecidableEq
 
--- This record printer intentionally ignores precedence.
-attribute [nolint unusedArguments] instReprThresholdOp.repr
 
 namespace ThresholdOp