doc(Circuit/Boolean): document public declarations and align module docs in Boolean circuit subdirectories (#590)

Complexity/Computability/Circuit/Boolean/ACC0/Basic.lean

@@ -88,6 +88,7 @@ def modZeroCircuit : (op : ExtOp) → Circuit Unbounded.signature (extSignature.
   | .ac op => Circuit.oneGate (σ := Unbounded.signature) op id
   | .gate m => Circuit.oneGate (σ := Unbounded.signature) (.or m) id
 
+/-- `modZeroCircuit op` computes the `AC⁰[0]` operation `op` over the `AC⁰` basis. -/
 theorem computes_modZeroCircuit (op : ExtOp) :
     (modZeroCircuit op).Computes Unbounded.interpretation
       (single (extInterpretation (modGate 0) op)) := by
@@ -112,6 +113,7 @@ def modOneCircuit : (op : ExtOp) → Circuit Unbounded.signature (extSignature.A
   | .ac op => Circuit.oneGate (σ := Unbounded.signature) op id
   | .gate _ => constCircuit (Signature.Hom.id _) false
 
+/-- `modOneCircuit op` computes the `AC⁰[1]` operation `op` over the `AC⁰` basis. -/
 theorem computes_modOneCircuit (op : ExtOp) :
     (modOneCircuit op).Computes Unbounded.interpretation
       (single (extInterpretation (modGate 1) op)) := by
@@ -155,6 +157,8 @@ def modMulCircuit (k : ℕ) : (op : ExtOp) → Circuit extSignature (extSignatur
   | .gate m => Circuit.oneGate (σ := extSignature) (.gate (m * k))
       fun j => (finProdFinEquiv.symm j).1
 
+/-- `modMulCircuit k op` computes the `AC⁰[q]` operation `op` over the `AC⁰[q * k]` basis when
+`0 < k`. -/
 theorem computes_modMulCircuit (q : ℕ) {k : ℕ} (hk : 0 < k) (op : ExtOp) :
     (modMulCircuit k op).Computes (extInterpretation (modGate (q * k)))
       (single (extInterpretation (modGate q) op)) := by

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

@@ -51,6 +51,8 @@ namespace State
 
 variable {n : ℕ} {f : BooleanFunction n}
 
+/-- A parameter `p` of degree `1` containing `H` among its children has `{H}` as its set of
+children. -/
 theorem children_eq_singleton {S : State n} {p : ℕ} {H : ℕ ⊕ ℕ} (h1 : S.deg p = 1)
     (hH : H ∈ S.children p) : S.children p = {H} := by
   obtain ⟨a, ha⟩ := Finset.card_eq_one.1 h1

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

@@ -33,6 +33,9 @@ elimination (`State.Valid.step_of_minimalAnd`):
 
 * `Cslib.Circuits.Boolean.AffineDisperser.State.SharedSecondChild`,
   `Cslib.Circuits.Boolean.AffineDisperser.State.Bottleneck`: the configurations of Section 4.3.
+* `Cslib.Circuits.Boolean.AffineDisperser.State.IsolatedBelow`,
+  `Cslib.Circuits.Boolean.AffineDisperser.State.fixInputDeleted`: unpaired isolated parameters
+  sharing a child with `G` and constraints deleted by fixing an input of `G`.
 
 ## Main results
 
@@ -242,6 +245,7 @@ weight when `G` becomes constant. -/
 def IsolatedBelow (S : State n) (G u : ℕ) : Prop :=
   u ∈ S.unpaired ∧ S.deg u = 1 ∧ ∃ N ∈ S.children G, N ∈ S.children u
 
+/-- Decidability of `State.IsolatedBelow`. -/
 instance (S : State n) (G : ℕ) : DecidablePred (S.IsolatedBelow G) :=
   fun _ => inferInstanceAs (Decidable (_ ∧ _ ∧ _))
 

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

@@ -30,7 +30,8 @@ child.
 
 ## Main definitions
 
-* `Cslib.Circuits.Boolean.AffineDisperser.State.auxIn`,
+* `Cslib.Circuits.Boolean.AffineDisperser.State.auxArgs`,
+  `Cslib.Circuits.Boolean.AffineDisperser.State.auxIn`,
   `Cslib.Circuits.Boolean.AffineDisperser.State.childIn`: the measures of the restructuring.
 * `Cslib.Circuits.Boolean.AffineDisperser.State.MinimalAnd`: the minimal AND.
 
@@ -487,13 +488,17 @@ namespace MinimalAnd
 
 variable {S : State n} {G x y : ℕ}
 
+/-- The first input `x` of a minimal AND is a parameter of `S`. -/
 theorem mem_params_x (h : S.MinimalAnd G x y) : x ∈ S.params := (mem_unpaired.1 h.unpaired_x).1
 
+/-- The second input `y` of a minimal AND is a parameter of `S`. -/
 theorem mem_params_y (h : S.MinimalAnd G x y) : y ∈ S.params := (mem_unpaired.1 h.unpaired_y).1
 
+/-- The minimal AND gate `G` is a child of its first input `x`. -/
 theorem mem_children_x (h : S.MinimalAnd G x y) : Sum.inl G ∈ S.children x :=
   (SemiCircuit.inl_mem_children _).2 ⟨h.mem, (Gate.reads_of_args h.args).1⟩
 
+/-- The minimal AND gate `G` is a child of its second input `y`. -/
 theorem mem_children_y (h : S.MinimalAnd G x y) : Sum.inl G ∈ S.children y :=
   (SemiCircuit.inl_mem_children _).2 ⟨h.mem, (Gate.reads_of_args h.args).2⟩
 
@@ -503,6 +508,7 @@ theorem exists_op (h : S.MinimalAnd G x y) : ∃ φ : Bool → Bool → Bool, ¬
   obtain ⟨φ, hφ, hG⟩ := Gate.exists_op_of_args h.args
   exact ⟨φ, fun h' => h.and_op (hφ.1 h'), hG⟩
 
+/-- No parameter of a valid state is equal to its minimal AND gate `G`. -/
 theorem ne_gate (hS : S.Valid f) (h : S.MinimalAnd G x y) {u : ℕ} (hu : u ∈ S.params) : u ≠ G :=
   fun he => hS.wf.notMem_gates_of_mem_params hu (he ▸ h.mem)
 

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

@@ -45,6 +45,8 @@ AND-type gate.
 * `Cslib.Circuits.Boolean.AffineDisperser.State.AndOnIsolated`, `State.DegeneratePair`,
   `State.PartnersShareChild`, `State.PairInSystem`, `State.AndOnPair`: the configurations of
   Cases 2 to 6.
+* `Cslib.Circuits.Boolean.AffineDisperser.State.Movable`, `State.freshEqn`: affine gates reading
+  no gates and a fresh equation name for moving them into the affine system.
 * `Cslib.Circuits.Boolean.AffineDisperser.State.Normal`: normal states.
 
 ## Main results
@@ -150,6 +152,7 @@ def Movable (S : State n) (J : ℕ) : Prop :=
 def freshEqn (S : State n) : ℕ :=
   S.eqns.sup id + 1
 
+/-- `S.freshEqn` is not an equation name of `S`. -/
 theorem freshEqn_notMem (S : State n) : S.freshEqn ∉ S.eqns := fun h => by
   have := Finset.le_sup (f := id) h
   simp only [id, freshEqn] at this

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

@@ -37,8 +37,9 @@ obligations `State.Transport` (`State.Valid.of_transport`).
 
 * `Cslib.Circuits.Boolean.AffineDisperser.State.Transport`: the obligations of transporting
   validity.
-* `Cslib.Circuits.Boolean.AffineDisperser.State.restrict`, `State.deleteGate`, `State.deleteEqn`,
-  `State.dropEqn`, `State.dropTrivialEqn`: the operations.
+* `Cslib.Circuits.Boolean.AffineDisperser.State.restrict`, `State.RestrictOK`,
+  `State.deleteGate`, `State.deleteEqn`, `State.dropEqn`, `State.dropTrivialEqn`: the operations
+  and the restriction hypotheses.
 
 ## Main results
 
@@ -58,6 +59,8 @@ namespace Cslib.Circuits.Boolean.AffineDisperser
 
 open Finset Cslib.BitString SemiCircuit
 
+/-- Evaluating a literal `ℓ` along an affine family of assignments `τ` defines an affine Boolean
+function. -/
 theorem isAffine_lit_eval {k : ℕ} {τ : BitString k → ℕ → Bool} (hτ : IsAffine τ) (ℓ : Lit) :
     IsAffine fun u => ℓ.eval (τ u) := by
   intro u v w
@@ -162,21 +165,27 @@ structure RestrictOK (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ
   avoid : ∀ pr ∈ P, pr.1 ≠ x ∧ pr.2 ≠ x
   drop : ∀ pr ∈ S.pairs, pr ∉ P → (pr.1 = x ∨ pr.2 = x) ∧ ∀ y, ℓ.Reads y → y = pr.1 ∨ y = pr.2
 
+/-- Restricting `x` removes `x` from the parameters of `S`. -/
 @[simp] theorem restrict_params (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) :
     (S.restrict x ℓ P).params = S.params.erase x := rfl
 
+/-- The pairs of `S.restrict x ℓ P` are `P`. -/
 @[simp] theorem restrict_pairs (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) :
     (S.restrict x ℓ P).pairs = P := rfl
 
+/-- The children of `z` in `S.restrict x ℓ P` are its children after substituting `x` with `ℓ`. -/
 theorem restrict_children (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) (z : ℕ) :
     (S.restrict x ℓ P).children z = (S.toSemiCircuit.subst x ℓ).children z := rfl
 
+/-- Restricting a parameter preserves the size of the state. -/
 theorem restrict_size (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) :
     (S.restrict x ℓ P).size = S.size := rfl
 
+/-- Restricting `x` to `ℓ` substitutes `x` with `ℓ` in every gate. -/
 @[simp] theorem restrict_gate (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) (J : ℕ) :
     (S.restrict x ℓ P).gate J = (S.gate J).subst x ℓ := rfl
 
+/-- Restricting `x` to `ℓ` substitutes `x` with `ℓ` in every equation. -/
 @[simp] theorem restrict_eqn (S : State n) (x : ℕ) (ℓ : Lit) (P : Finset (ℕ × ℕ)) (e : ℕ) :
     (S.restrict x ℓ P).eqn e = (S.eqn e).subst x ℓ := rfl
 
@@ -254,31 +263,40 @@ theorem Valid.restrict {S : State n} (hS : S.Valid f) {x : ℕ} {ℓ : Lit} {P :
 def deleteGate (S : State n) (J : ℕ) (ℓ : Lit) : State n :=
   { S with toSemiCircuit := S.toSemiCircuit.deleteGate J ℓ }
 
+/-- Deleting a gate preserves the parameters of the state. -/
 @[simp] theorem deleteGate_params (S : State n) (J : ℕ) (ℓ : Lit) :
     (S.deleteGate J ℓ).params = S.params := rfl
 
+/-- Deleting a gate preserves the pairs of the state. -/
 @[simp] theorem deleteGate_pairs (S : State n) (J : ℕ) (ℓ : Lit) :
     (S.deleteGate J ℓ).pairs = S.pairs := rfl
 
+/-- Deleting a gate preserves the parameter map `phi`. -/
 @[simp] theorem deleteGate_phi (S : State n) (J : ℕ) (ℓ : Lit) :
     (S.deleteGate J ℓ).phi = S.phi := rfl
 
+/-- Deleting gate `J` with replacement `ℓ` substitutes `J` with `ℓ` in every gate. -/
 @[simp] theorem deleteGate_gate (S : State n) (J : ℕ) (ℓ : Lit) (K : ℕ) :
     (S.deleteGate J ℓ).gate K = (S.gate K).subst J ℓ := rfl
 
+/-- Deleting gate `J` with replacement `ℓ` substitutes `J` with `ℓ` in every equation. -/
 @[simp] theorem deleteGate_eqn (S : State n) (J : ℕ) (ℓ : Lit) (e : ℕ) :
     (S.deleteGate J ℓ).eqn e = (S.eqn e).subst J ℓ := rfl
 
+/-- Deleting gate `J` removes `J` from `S.gates`. -/
 @[simp] theorem deleteGate_gates (S : State n) (J : ℕ) (ℓ : Lit) :
     (S.deleteGate J ℓ).gates = S.gates.erase J := rfl
 
+/-- Deleting a gate decreases the size of the state by `1`. -/
 theorem deleteGate_size {S : State n} {J : ℕ} {ℓ : Lit}
     (h : S.DeleteGateOK J ℓ) : (S.deleteGate J ℓ).size + 1 = S.size := by
   have := Finset.card_erase_add_one h.mem
   simp only [SemiCircuit.size] at *
   change (S.gates.erase J).card + S.eqns.card + 1 = _
   omega
 
+/-- After deleting gate `J` with replacement `ℓ`, the children of `z` are contained in the
+children of `z` after substituting `J` with `ℓ` with `.inl J` removed. -/
 theorem deleteGate_children_subset {S : State n} {J : ℕ} {ℓ : Lit} (z : ℕ) :
     (S.deleteGate J ℓ).children z ⊆ ((S.toSemiCircuit.subst J ℓ).children z).erase (.inl J) := by
   intro w hw
@@ -311,22 +329,28 @@ to `ℓ`. -/
 def deleteEqn (S : State n) (e v : ℕ) (ℓ : Lit) : State n :=
   { S with toSemiCircuit := S.toSemiCircuit.deleteEqn e v ℓ }
 
+/-- Deleting an equation preserves the parameters of the state. -/
 @[simp] theorem deleteEqn_params (S : State n) (e v : ℕ) (ℓ : Lit) :
     (S.deleteEqn e v ℓ).params = S.params := rfl
 
+/-- Deleting an equation preserves the pairs of the state. -/
 @[simp] theorem deleteEqn_pairs (S : State n) (e v : ℕ) (ℓ : Lit) :
     (S.deleteEqn e v ℓ).pairs = S.pairs := rfl
 
+/-- Deleting an equation preserves the parameter map `phi`. -/
 @[simp] theorem deleteEqn_phi (S : State n) (e v : ℕ) (ℓ : Lit) :
     (S.deleteEqn e v ℓ).phi = S.phi := rfl
 
+/-- Deleting an equation decreases the size of the state by `1`. -/
 theorem deleteEqn_size {S : State n} {e v : ℕ} {ℓ : Lit} (h : S.DeleteEqnOK e v ℓ) :
     (S.deleteEqn e v ℓ).size + 1 = S.size := by
   have := Finset.card_erase_add_one h.mem
   simp only [SemiCircuit.size] at *
   change S.gates.card + (S.eqns.erase e).card + 1 = _
   omega
 
+/-- After deleting equation `e` and auxiliary variable `v` with replacement `ℓ`, the children of
+`z` are contained in the children of `z` after substituting `v` with `ℓ` with `.inr e` removed. -/
 theorem deleteEqn_children_subset {S : State n} {e v : ℕ} {ℓ : Lit} (z : ℕ) :
     (S.deleteEqn e v ℓ).children z ⊆ ((S.toSemiCircuit.subst v ℓ).children z).erase (.inr e) := by
   intro w hw
@@ -338,6 +362,8 @@ theorem deleteEqn_children_subset {S : State n} {e v : ℕ} {ℓ : Lit} (z : ℕ
     · cases he; exact Finset.notMem_erase e _ hw.1
     · exact (SemiCircuit.inr_mem_children _).2 ⟨Finset.mem_of_mem_erase hw.1, hw.2⟩
 
+/-- Deleting an equation removes it from the children of every parameter other than the target of
+`ℓ`. -/
 theorem deleteEqn_children_of_ne {S : State n} (hS : S.Valid f) {e v : ℕ} {ℓ : Lit}
     (h : S.DeleteEqnOK e v ℓ) {z : ℕ} (hz : z ∈ S.params) (hzℓ : ¬ ℓ.Reads z) :
     (S.deleteEqn e v ℓ).children z ⊆ (S.children z).erase (.inr e) := by
@@ -356,17 +382,21 @@ theorem Valid.deleteEqn {S : State n} (hS : S.Valid f) {e v : ℕ} {ℓ : Lit}
 def dropEqn (S : State n) (e v : ℕ) : State n :=
   { S with toSemiCircuit := S.toSemiCircuit.dropEqn e v }
 
+/-- Dropping an equation preserves the parameters of the state. -/
 @[simp] theorem dropEqn_params (S : State n) (e v : ℕ) : (S.dropEqn e v).params = S.params := rfl
 
+/-- Dropping an equation preserves the pairs of the state. -/
 @[simp] theorem dropEqn_pairs (S : State n) (e v : ℕ) : (S.dropEqn e v).pairs = S.pairs := rfl
 
+/-- Dropping an equation decreases the size of the state by `1`. -/
 theorem dropEqn_size {S : State n} {e v : ℕ} (h : S.DropEqnOK e v) :
     (S.dropEqn e v).size + 1 = S.size := by
   have := Finset.card_erase_add_one h.mem
   simp only [SemiCircuit.size] at *
   change S.gates.card + (S.eqns.erase e).card + 1 = _
   omega
 
+/-- Dropping equation `e` removes `.inr e` from the children of `z`. -/
 theorem dropEqn_children (S : State n) (e v z : ℕ) :
     (S.dropEqn e v).children z = (S.children z).erase (.inr e) := by
   ext (K | e')
@@ -387,19 +417,23 @@ theorem Valid.dropEqn {S : State n} (hS : S.Valid f) {e v : ℕ} (h : S.DropEqnO
 def dropTrivialEqn (S : State n) (e : ℕ) : State n :=
   { S with toSemiCircuit := S.toSemiCircuit.dropTrivialEqn e }
 
+/-- Dropping a trivial equation preserves the parameters of the state. -/
 @[simp] theorem dropTrivialEqn_params (S : State n) (e : ℕ) :
     (S.dropTrivialEqn e).params = S.params := rfl
 
+/-- Dropping a trivial equation preserves the pairs of the state. -/
 @[simp] theorem dropTrivialEqn_pairs (S : State n) (e : ℕ) :
     (S.dropTrivialEqn e).pairs = S.pairs := rfl
 
+/-- Dropping a trivial equation decreases the size of the state by `1`. -/
 theorem dropTrivialEqn_size {S : State n} {e : ℕ} (he : e ∈ S.eqns) :
     (S.dropTrivialEqn e).size + 1 = S.size := by
   have := Finset.card_erase_add_one he
   simp only [SemiCircuit.size] at *
   change S.gates.card + (S.eqns.erase e).card + 1 = _
   omega
 
+/-- Dropping trivial equation `e` removes `.inr e` from the children of `z`. -/
 theorem dropTrivialEqn_children (S : State n) (e z : ℕ) :
     (S.dropTrivialEqn e).children z = (S.children z).erase (.inr e) := by
   ext (K | e')

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

@@ -159,6 +159,7 @@ namespace Reduction
 
 variable {S S' : State n} {F : Finset ℕ} {D T : List (ℕ ⊕ ℕ)}
 
+/-- The empty reduction from a valid state `S` to itself. -/
 theorem refl (hS : S.Valid f) : Reduction f S S ∅ [] [] where
   valid := hS
   subset := Finset.empty_subset _
@@ -214,20 +215,25 @@ theorem mono (h : Reduction f S S' F D T) {T' : List (ℕ ⊕ ℕ)} (hT : ∀ N
 
 /-! ### Accounting -/
 
+/-- A reduction restricting `F` decreases the number of parameters `m` by `|F|`. -/
 theorem m_add (h : Reduction f S S' F D T) : S'.m + F.card = S.m := by
   unfold m
   rw [h.params, Finset.card_sdiff_of_subset h.subset]
   have := Finset.card_le_card h.subset
   omega
 
+/-- A reduction deleting `D` decreases the size `s` by `|D|`. -/
 theorem s_add (h : Reduction f S S' F D T) : S'.s + D.length = S.s :=
   h.size
 
+/-- A reduction restricting `F` decreases the number of pairs `q` by the number of pairs meeting
+`F`. -/
 theorem q_add (h : Reduction f S S' F D T) : S'.q + (S.pairsMeeting F).card = S.q := by
   unfold q pairsMeeting
   rw [h.pairs, add_comm]
   exact Finset.card_filter_add_card_filter_not _
 
+/-- Under a reduction restricting `F`, `S'.a + |F| = S.a + (S.pairsMeeting F).card`. -/
 theorem a_add (h : Reduction f S S' F D T) (hS : S.Valid f) :
     S'.a + F.card = S.a + (S.pairsMeeting F).card := by
   have hm := h.m_add
@@ -465,21 +471,27 @@ private theorem restrictOK_fixConst {S : State n} {w : ℕ} (hw : w ∈ S.params
     push Not at h
     exact hP (Finset.mem_filter.2 ⟨hpr, h⟩)
 
+/-- Fixing a parameter to a constant preserves validity. -/
 theorem Valid.fixConst {S : State n} (hS : S.Valid f) {w : ℕ} (hw : w ∈ S.params) (b : Bool) :
     (S.fixConst w b).Valid f :=
   hS.restrict (restrictOK_fixConst hw b)
 
+/-- Fixing `w` to a constant removes `w` from `S.params`. -/
 @[simp] theorem fixConst_params (S : State n) (w : ℕ) (b : Bool) :
     (S.fixConst w b).params = S.params.erase w := rfl
 
+/-- Fixing `w` to a constant retains the pairs avoiding `w`. -/
 @[simp] theorem fixConst_pairs (S : State n) (w : ℕ) (b : Bool) :
     (S.fixConst w b).pairs = S.pairsAvoid w := rfl
 
+/-- Fixing a parameter to a constant preserves the size of the state. -/
 theorem fixConst_size (S : State n) (w : ℕ) (b : Bool) : (S.fixConst w b).size = S.size := rfl
 
+/-- Fixing `w` to `b` substitutes `w` with `Lit.const b` in every gate. -/
 @[simp] theorem fixConst_gate (S : State n) (w : ℕ) (b : Bool) (J : ℕ) :
     (S.fixConst w b).gate J = (S.gate J).subst w (Lit.const b) := rfl
 
+/-- Fixing `w` to a constant preserves the children of every `z ≠ w`. -/
 theorem fixConst_children (S : State n) {w : ℕ} (b : Bool) {z : ℕ} (hz : z ≠ w) :
     (S.fixConst w b).children z = S.children z :=
   SemiCircuit.children_subst hz (by simp [Lit.const])

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

@@ -28,7 +28,10 @@ parameter map is unchanged:
 ## Main definitions
 
 * `Cslib.Circuits.Boolean.AffineDisperser.State.swap`,
-  `Cslib.Circuits.Boolean.AffineDisperser.State.quad`: the reparameterisations.
+  `Cslib.Circuits.Boolean.AffineDisperser.State.SwapOK`,
+  `Cslib.Circuits.Boolean.AffineDisperser.State.quad`,
+  `Cslib.Circuits.Boolean.AffineDisperser.State.QuadOK`: the reparameterisations and their
+  hypotheses.
 
 ## Main results
 
@@ -69,15 +72,19 @@ structure SwapOK (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) : Prop wh
   affine : S.AffineIn Q c T
   mem_T : x ∈ T
 
+/-- Exchanging `x` and `Q` replaces `x` with `Q` in `S.params`. -/
 @[simp] theorem swap_params (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) :
     (S.swap x Q c T).params = insert Q (S.params.erase x) := rfl
 
+/-- Exchanging `x` and `Q` preserves the pairs of the state. -/
 @[simp] theorem swap_pairs (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) :
     (S.swap x Q c T).pairs = S.pairs := rfl
 
+/-- Exchanging `x` and `Q` preserves the size of the state. -/
 theorem swap_size (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) :
     (S.swap x Q c T).size = S.size := rfl
 
+/-- Exchanging `x` and `Q` preserves the children of every variable. -/
 theorem swap_children (S : State n) (x Q : ℕ) (c : Bool) (T : Finset ℕ) (z : ℕ) :
     (S.swap x Q c T).children z = S.children z := rfl
 
@@ -187,12 +194,15 @@ structure QuadOK (S : State n) (x y z G D : ℕ) (α β γ c : Bool) : Prop
   unpaired_y : ¬ S.Paired y
   unpaired_z : ¬ S.Paired z
 
+/-- The quadratic reparameterisation replaces `z` with `D` in `S.params`. -/
 @[simp] theorem quad_params (S : State n) (x y z G D : ℕ) (α β γ c : Bool) :
     (S.quad x y z G D α β γ c).params = insert D (S.params.erase z) := rfl
 
+/-- The quadratic reparameterisation inserts `(x, y)` into `S.pairs`. -/
 @[simp] theorem quad_pairs (S : State n) (x y z G D : ℕ) (α β γ c : Bool) :
     (S.quad x y z G D α β γ c).pairs = insert (x, y) S.pairs := rfl
 
+/-- The quadratic reparameterisation decreases the size of the state by `2`. -/
 theorem quad_size {S : State n} {x y z G D : ℕ} {α β γ c : Bool}
     (h : S.QuadOK x y z G D α β γ c) : (S.quad x y z G D α β γ c).size + 2 = S.size := by
   have h1 := Finset.card_erase_add_one h.mem_D
@@ -201,6 +211,8 @@ theorem quad_size {S : State n} {x y z G D : ℕ} {α β γ c : Bool}
   change ((S.gates.erase D).erase G).card + S.eqns.card + 2 = _
   omega
 
+/-- After the quadratic reparameterisation, the children of `w` are contained in `S.children w`
+with `.inl D` and `.inl G` removed. -/
 theorem quad_children_subset (S : State n) (x y z G D : ℕ) (α β γ c : Bool) (w : ℕ) :
     (S.quad x y z G D α β γ c).children w ⊆ ((S.children w).erase (.inl D)).erase (.inl G) := by
   intro v hv