States of gate elimination and their potential

A state of the gate elimination of Mishra and Santhanam, Section 2.4 for a Boolean function f on n bits consists of a fair semi-circuit reading parameters, a set of disjoint pairs of parameters and an injective map Φ from parameter values to inputs of f such that the semi-circuit computes f ∘ Φ (State.Valid). The source keeps Φ in the form

Φ(u) = b + L u + ∑_{{p, r} ∈ P} c_{pr} p r (form (1) of the source),

an affine map plus quadratic terms over the pairs. We record only the property of this form that the proof uses: along every affine family of parameter assignments on which each pair has a constant member, or a constant sum, Φ is affine (State.Valid.phi_affine). The map Φ is stored as a function of all internal values that depends only on the parameters.

A state has m parameters, q pairs, a = m - q and size s, the number of gates plus the number of equations. The weight of an unpaired parameter of degree k is 0, 6 or 7 for k = 0, k = 1 and k ≥ 2, and the potential is

W = 2 s + 3 q + ∑_{x unpaired} wt(x) (equation (5) of the source).

Proposition 2.2 of the source: the image of Φ contains the image of an injective affine map from BitString a, informally an affine subspace of dimension a (State.Valid.exists_affine_embedding), so the output of a valid state for an affine disperser for dimension d ≤ a is not constant (State.Valid.exists_out_ne_of_le). Restricting one more parameter to an affine function of the others keeps dimension a - 1, so when d < a the output is not constant there either (State.Valid.false_of_fix); in particular it is not an affine function of the parameters (State.Valid.out_not_affine, part of Lemma 2.3 of the source).

Writing State.wt S x for the weight of x if it is an unpaired parameter of S and 0 otherwise, the potentials of two states compare name by name (State.W_add_le). A step of gate elimination (State.Step) is a move to a valid state with smaller m + s, Δa ∈ {0, -1, -2} and ΔW ≤ 14 Δa, as in Lemma 4.2 of the source; a preparatory operation (State.Preparation) keeps m, s and q and does not increase W.

Main definitions

• Cslib.Circuits.Boolean.AffineDisperser.State, Cslib.Circuits.Boolean.AffineDisperser.State.Valid: states.
• Cslib.Circuits.Boolean.AffineDisperser.State.m, q, a, s, W: the counted quantities and the potential, with Cslib.Circuits.Boolean.AffineDisperser.weight.
• Cslib.Circuits.Boolean.AffineDisperser.State.Step, Cslib.Circuits.Boolean.AffineDisperser.State.Preparation: steps and preparatory operations.
• Cslib.Circuits.Boolean.AffineDisperser.State.IsPartner, Cslib.Circuits.Boolean.AffineDisperser.State.pairsMeeting: partners and the pairs meeting a set of parameters.

Main results

• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_affine_embedding: Proposition 2.2.
• Cslib.Circuits.Boolean.AffineDisperser.State.Valid.false_of_fix, Cslib.Circuits.Boolean.AffineDisperser.State.Valid.out_not_affine: Lemma 2.3.
• Cslib.Circuits.Boolean.AffineDisperser.State.W_add_le: comparing potentials name by name.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits

def Cslib.Circuits.Boolean.AffineDisperser.weight (k : ℕ) : ℕ

The weight of an unpaired parameter of degree k: 0 if it is unused, 6 if it is isolated and 7 otherwise (equation (4) of Mishra and Santhanam).

theorem Cslib.Circuits.Boolean.AffineDisperser.weight_mono {k l : ℕ} (h : k ≤ l) : weight k ≤ weight l

theorem Cslib.Circuits.Boolean.AffineDisperser.weight_le_seven (k : ℕ) : weight k ≤ 7

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.weight_zero : weight 0 = 0

@[simp]

theorem Cslib.Circuits.Boolean.AffineDisperser.weight_one : weight 1 = 6

theorem Cslib.Circuits.Boolean.AffineDisperser.weight_of_two_le {k : ℕ} (hk : 2 ≤ k) : weight k = 7

theorem Cslib.Circuits.Boolean.AffineDisperser.six_le_weight {k : ℕ} (hk : 1 ≤ k) : 6 ≤ weight k

def Cslib.Circuits.Boolean.AffineDisperser.PairTame {α : Type u_1} (σ : α → ℕ → Bool) (pr : ℕ × ℕ) : Prop

Along the family σ of assignments, the pair pr contributes an affine term to a quadratic map: one of its members, or their sum, is constant.

structure Cslib.Circuits.Boolean.AffineDisperser.State (n : ℕ) extends Cslib.Circuits.Boolean.SemiCircuit : Type

A state of gate elimination for a function of n bits: a semi-circuit, disjoint pairs of parameters and the parameter map Φ.

• params : Finset ℕ
• aux : Finset ℕ
• gates : Finset ℕ
• gate : ℕ → Gate
• eqns : Finset ℕ
• eqn : ℕ → Equation
• out : Lit
• pairs : Finset (ℕ × ℕ)

  The pairs of parameters that may occur together in a quadratic term of Φ.

• phi : (ℕ → Bool) → BitString n

  The parameter map, as a function of the values of all internal values.

def Cslib.Circuits.Boolean.AffineDisperser.State.Paired {n : ℕ} (S : State n) (x : ℕ) : Prop

x belongs to one of the pairs.

@[instance_reducible]

instance Cslib.Circuits.Boolean.AffineDisperser.State.instDecidablePredNatPaired {n : ℕ} (S : State n) : DecidablePred S.Paired

def Cslib.Circuits.Boolean.AffineDisperser.State.unpaired {n : ℕ} (S : State n) : Finset ℕ

The unpaired parameters.

def Cslib.Circuits.Boolean.AffineDisperser.State.m {n : ℕ} (S : State n) : ℕ

The number of parameters.

def Cslib.Circuits.Boolean.AffineDisperser.State.q {n : ℕ} (S : State n) : ℕ

The number of pairs.

def Cslib.Circuits.Boolean.AffineDisperser.State.a {n : ℕ} (S : State n) : ℕ

The number of parameters minus the number of pairs.

def Cslib.Circuits.Boolean.AffineDisperser.State.s {n : ℕ} (S : State n) : ℕ

The size of the semi-circuit: gates plus equations.

def Cslib.Circuits.Boolean.AffineDisperser.State.W {n : ℕ} (S : State n) : ℕ

The potential W = 2 s + 3 q + ∑ wt(x) over the unpaired parameters x.

structure Cslib.Circuits.Boolean.AffineDisperser.State.Valid {n : ℕ} (S : State n) (f : BooleanFunction n) : Prop

A valid state for f: a well-formed fair semi-circuit, disjoint pairs of distinct parameters, and an injective parameter map that depends only on the parameters and is affine along every affine family of assignments on which each pair has a constant member or a constant sum, such that the output of every consistent assignment is the value of f at its image.

• wf : S.WellFormed

  The semi-circuit is well formed.

• pair_mem (pr : ℕ × ℕ) : pr ∈ S.pairs → pr.1 ∈ S.params ∧ pr.2 ∈ S.params ∧ pr.1 ≠ pr.2

  Pairs consist of two distinct parameters.

• pairs_disjoint (pr : ℕ × ℕ) : pr ∈ S.pairs → ∀ pr' ∈ S.pairs, pr ≠ pr' → pr.1 ≠ pr'.1 ∧ pr.1 ≠ pr'.2 ∧ pr.2 ≠ pr'.1 ∧ pr.2 ≠ pr'.2

  Distinct pairs are disjoint.

• phi_congr (val val' : ℕ → Bool) : (∀ j ∈ S.params, val j = val' j) → S.phi val = S.phi val'

  The parameter map depends only on the parameters.

• phi_affine (k : ℕ) (σ : BitString k → ℕ → Bool) : BitString.IsAffine σ → (∀ pr ∈ S.pairs, PairTame σ pr) → BitString.IsAffine (S.phi ∘ σ)

  The parameter map is affine along affine families on which every pair is tame.

• phi_injective (val val' : ℕ → Bool) : S.phi val = S.phi val' → ∀ j ∈ S.params, val j = val' j

  The parameter map is injective on the parameters.

• computes (val : ℕ → Bool) : S.Consistent val → S.out.eval val = f (S.phi val)

  Every consistent assignment outputs f at its image.

Spreading bits over a finite set of names

def Cslib.Circuits.Boolean.AffineDisperser.State.spread (F : Finset ℕ) {k : ℕ} (h : F.card = k) (u : BitString k) : ℕ → Bool

The assignment reading the bits of u on the elements of F, in increasing order, and false elsewhere.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.isAffine_spread (F : Finset ℕ) {k : ℕ} (h : F.card = k) : BitString.IsAffine (spread F h)

theorem Cslib.Circuits.Boolean.AffineDisperser.State.spread_of_notMem {F : Finset ℕ} {k : ℕ} (h : F.card = k) (u : BitString k) {i : ℕ} (hi : i ∉ F) : spread F h u i = false

theorem Cslib.Circuits.Boolean.AffineDisperser.State.spread_orderIsoOfFin {F : Finset ℕ} {k : ℕ} (h : F.card = k) (u : BitString k) (i : Fin k) : spread F h u ↑((F.orderIsoOfFin h) i) = u i

theorem Cslib.Circuits.Boolean.AffineDisperser.State.eq_of_spread {F : Finset ℕ} {k : ℕ} (h : F.card = k) {u v : BitString k} (huv : ∀ i ∈ F, spread F h u i = spread F h v i) : u = v

theorem Cslib.Circuits.Boolean.AffineDisperser.State.isAffine_update {k : ℕ} {σ : BitString k → ℕ → Bool} (hσ : BitString.IsAffine σ) (x : ℕ) {ψ : BitString k → Bool} (hψ : BitString.IsAffine ψ) : BitString.IsAffine fun (u : BitString k) => Function.update (σ u) x (ψ u)

Updating an affine family at one name by an affine function keeps it affine.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.isAffine_const_add_sum {k : ℕ} {σ : BitString k → ℕ → Bool} (hσ : BitString.IsAffine σ) (c : Bool) (R : Finset ℕ) : BitString.IsAffine fun (u : BitString k) => c + ∑ j ∈ R, σ u j

A constant plus a sum of coordinates of an affine family is affine.

Proposition 2.2

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.card_sdiff_image {n : ℕ} {S : State n} {f : BooleanFunction n} (hS : S.Valid f) (rep : ℕ × ℕ → ℕ) (hrep : ∀ (pr : ℕ × ℕ), rep pr = pr.1 ∨ rep pr = pr.2) : (S.params \ Finset.image rep S.pairs).card = S.a

Choosing one member rep pr of every pair leaves exactly a other parameters.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_out_ne {n : ℕ} {S : State n} {f : BooleanFunction n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) {k : ℕ} (σ : BitString k → ℕ → Bool) (hσ : BitString.IsAffine σ) (htame : ∀ pr ∈ S.pairs, PairTame σ pr) (hinj : ∀ (u v : BitString k), (∀ j ∈ S.params, σ u j = σ v j) → u = v) (hk : d ≤ k) : ∃ (u : BitString k) (v : BitString k) (val : ℕ → Bool) (val' : ℕ → Bool), S.Consistent val ∧ S.Consistent val' ∧ (∀ j ∈ S.params, val j = σ u j) ∧ (∀ j ∈ S.params, val' j = σ v j) ∧ S.out.eval val ≠ S.out.eval val'

Along an injective affine family of parameter assignments on which every pair is tame, the parameter map is an injective affine map, so the output of a valid state for an affine disperser for dimension d is not constant when the family has dimension at least d.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_affine_embedding {n : ℕ} {S : State n} {f : BooleanFunction n} (hS : S.Valid f) : ∃ (g : BitString S.a → BitString n), BitString.IsAffine g ∧ Function.Injective g ∧ ∀ (u : BitString S.a), ∃ (val : ℕ → Bool), S.Consistent val ∧ g u = S.phi val

Proposition 2.2 of Mishra and Santhanam: the image of the parameter map of a valid state contains the image of an injective affine map from BitString a.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.exists_out_ne_of_le {n : ℕ} {S : State n} {f : BooleanFunction n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d ≤ S.a) : ∃ (val : ℕ → Bool) (val' : ℕ → Bool), S.Consistent val ∧ S.Consistent val' ∧ S.out.eval val ≠ S.out.eval val'

The output of a valid state for an affine disperser for dimension d ≤ a is not constant.

Lemma 2.3

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.false_of_fix {n : ℕ} {S : State n} {f : BooleanFunction n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) {x : ℕ} (hx : x ∈ S.params) (c : Bool) (R : Finset ℕ) (hR : R ⊆ S.params) (hxR : x ∉ R) (b : Bool) (hout : ∀ (val : ℕ → Bool), S.Consistent val → val x = c + ∑ j ∈ R, val j → S.out.eval val = b) : False

If d < a, the output of a valid state for an affine disperser for dimension d is not constant on the consistent assignments satisfying one more affine equation x = c + ∑ j ∈ R, u j between the parameters: imposing it keeps an affine subspace of dimension a - 1 ≥ d in the image of the parameter map.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.out_not_affine {n : ℕ} {S : State n} {f : BooleanFunction n} {d : ℕ} (hS : S.Valid f) (hf : BitString.IsAffineDisperser f d) (ha : d < S.a) (c : Bool) {T : Finset ℕ} (hT : T ⊆ S.params) : ¬∀ (val : ℕ → Bool), S.Consistent val → S.out.eval val = c + ∑ j ∈ T, val j

Part of Lemma 2.3 of Mishra and Santhanam: if d < a, the output of a valid state for an affine disperser for dimension d is not an affine function of the parameters.

Bookkeeping for the potential

def Cslib.Circuits.Boolean.AffineDisperser.State.wt {n : ℕ} (S : State n) (x : ℕ) : ℕ

The weight contributed by the name x: its weight if it is an unpaired parameter, and 0 otherwise.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.wt_le_seven {n : ℕ} (S : State n) (x : ℕ) : S.wt x ≤ 7

theorem Cslib.Circuits.Boolean.AffineDisperser.State.mem_unpaired {n : ℕ} {S : State n} {x : ℕ} : x ∈ S.unpaired ↔ x ∈ S.params ∧ ¬S.Paired x

theorem Cslib.Circuits.Boolean.AffineDisperser.State.wt_of_mem {n : ℕ} {S : State n} {x : ℕ} (hx : x ∈ S.unpaired) : S.wt x = weight (S.deg x)

theorem Cslib.Circuits.Boolean.AffineDisperser.State.wt_of_notMem {n : ℕ} {S : State n} {x : ℕ} (hx : x ∉ S.unpaired) : S.wt x = 0

theorem Cslib.Circuits.Boolean.AffineDisperser.State.wt_of_paired {n : ℕ} {S : State n} {x : ℕ} (hx : S.Paired x) : S.wt x = 0

theorem Cslib.Circuits.Boolean.AffineDisperser.State.wt_of_notMem_params {n : ℕ} {S : State n} {x : ℕ} (hx : x ∉ S.params) : S.wt x = 0

theorem Cslib.Circuits.Boolean.AffineDisperser.State.sum_wt {n : ℕ} (S : State n) {N : Finset ℕ} (hN : S.params ⊆ N) : ∑ x ∈ N, S.wt x = ∑ x ∈ S.unpaired, weight (S.deg x)

theorem Cslib.Circuits.Boolean.AffineDisperser.State.W_eq_sum {n : ℕ} (S : State n) {N : Finset ℕ} (hN : S.params ⊆ N) : S.W = 2 * S.s + 3 * S.q + ∑ x ∈ N, S.wt x

theorem Cslib.Circuits.Boolean.AffineDisperser.State.W_add_le {n : ℕ} {S S' : State n} {N : Finset ℕ} (hN : S.params ⊆ N) (hN' : S'.params ⊆ N) (loss gain : ℕ → ℕ) (h : ∀ x ∈ N, S'.wt x + loss x ≤ S.wt x + gain x) : S'.W + 2 * S.s + 3 * S.q + ∑ x ∈ N, loss x ≤ S.W + 2 * S'.s + 3 * S'.q + ∑ x ∈ N, gain x

Potentials compare name by name: if every name of a common set loses loss x and gains at most gain x in weight, the sums of losses and gains bound the change of potential.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.mem_unpaired_of {n : ℕ} {S S' : State n} {x : ℕ} (hx : x ∈ S'.unpaired) (hp : x ∈ S.params) (hpairs : S.pairs ⊆ S'.pairs) : x ∈ S.unpaired

Unpaired parameters of a state with the same pairs and fewer parameters were unpaired.

structure Cslib.Circuits.Boolean.AffineDisperser.State.Step {n : ℕ} (f : BooleanFunction n) (S S' : State n) : Prop

A step of gate elimination from S to S', as in Lemma 4.2 of Mishra and Santhanam: S' is valid, m + s decreases, Δa ∈ {0, -1, -2} and ΔW ≤ 14 Δa, written without subtraction.

• valid : S'.Valid f

  The new state is valid.

• lt : S'.m + S'.s < S.m + S.s

  m + s decreases.

• a_le : S'.a ≤ S.a

  a does not increase.

• le_a : S.a ≤ S'.a + 2

  a decreases by at most two.

• potential : S'.W + 14 * S.a ≤ S.W + 14 * S'.a

  ΔW ≤ 14 Δa.

structure Cslib.Circuits.Boolean.AffineDisperser.State.Preparation {n : ℕ} (f : BooleanFunction n) (S S' : State n) : Prop

A preparatory operation of gate elimination from S to S': S' is valid, with the same m, s and q as S and no larger potential.

• valid : S'.Valid f

  The new state is valid.

• m_eq : S'.m = S.m

  The number of parameters is kept.

• s_eq : S'.s = S.s

  The size is kept.

• q_eq : S'.q = S.q

  The number of pairs is kept.

• W_le : S'.W ≤ S.W

  The potential does not increase.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Preparation.a_eq {n : ℕ} {f : BooleanFunction n} {S S' : State n} (h : Preparation f S S') : S'.a = S.a

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Step.of_preparation {n : ℕ} {f : BooleanFunction n} {S S₁ S' : State n} (hp : Preparation f S S₁) (h : Step f S₁ S') : Step f S S'

A preparatory operation followed by a step is a step.

Pairs and partners

def Cslib.Circuits.Boolean.AffineDisperser.State.IsPartner {n : ℕ} (S : State n) (w r : ℕ) : Prop

r is the partner of w: they form a pair.

@[instance_reducible]

instance Cslib.Circuits.Boolean.AffineDisperser.State.instDecidablePredNatIsPartner {n : ℕ} (S : State n) (w : ℕ) : DecidablePred (S.IsPartner w)

def Cslib.Circuits.Boolean.AffineDisperser.State.pairsAvoid {n : ℕ} (S : State n) (w : ℕ) : Finset (ℕ × ℕ)

The pairs avoiding w.

def Cslib.Circuits.Boolean.AffineDisperser.State.pairsMeeting {n : ℕ} (S : State n) (F : Finset ℕ) : Finset (ℕ × ℕ)

The pairs with a member in F.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.paired_congr {n : ℕ} {S S' : State n} (h : S'.pairs = S.pairs) {x : ℕ} : S'.Paired x ↔ S.Paired x

theorem Cslib.Circuits.Boolean.AffineDisperser.State.unpaired_congr {n : ℕ} {S S' : State n} (hp : S'.params = S.params) (h : S'.pairs = S.pairs) : S'.unpaired = S.unpaired

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.mem_params_of_paired {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {p : ℕ} (hp : S.Paired p) : p ∈ S.params

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.pair_unique {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {w : ℕ} {pr pr' : ℕ × ℕ} (hpr : pr ∈ S.pairs) (hpr' : pr' ∈ S.pairs) (h : pr.1 = w ∨ pr.2 = w) (h' : pr'.1 = w ∨ pr'.2 = w) : pr = pr'

A pair containing w is unique.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.exists_partner {n : ℕ} {S : State n} {p : ℕ} (hp : S.Paired p) : ∃ (r : ℕ), S.IsPartner p r

theorem Cslib.Circuits.Boolean.AffineDisperser.State.IsPartner.symm {n : ℕ} {S : State n} {p r : ℕ} (h : S.IsPartner p r) : S.IsPartner r p

theorem Cslib.Circuits.Boolean.AffineDisperser.State.IsPartner.paired {n : ℕ} {S : State n} {w r : ℕ} (h : S.IsPartner w r) : S.Paired w

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.partner_ne {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {p r : ℕ} (h : S.IsPartner p r) : r ≠ p

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.partner_mem {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {p r : ℕ} (h : S.IsPartner p r) : r ∈ S.params

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.isPartner_unique {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {w r r' : ℕ} (h : S.IsPartner w r) (h' : S.IsPartner w r') : r = r'

A partner is unique.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.sum_partner_le {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (w : ℕ) (N : Finset ℕ) (c : ℕ) : (∑ x ∈ N, if S.IsPartner w x then c else 0) ≤ c

The partners of w contribute at most one summand.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.paired_filter_iff {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {F : Finset ℕ} {u : ℕ} (huF : u ∉ F) : (∃ pr ∈ {pr ∈ S.pairs | ¬(pr.1 ∈ F ∨ pr.2 ∈ F)}, pr.1 = u ∨ pr.2 = u) ↔ S.Paired u ∧ ∀ x ∈ F, ¬S.IsPartner u x

A paired parameter outside F is in a pair meeting F exactly when its partner is in F.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.q_le_m {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) : S.q ≤ S.m

The parameters of a valid state are at least as many as its pairs.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.card_pairsMeeting_le {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (F : Finset ℕ) : (S.pairsMeeting F).card ≤ F.card

At most |F| pairs meet a set F of parameters.

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.card_pairsMeeting_singleton {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) (w : ℕ) : (S.pairsMeeting {w}).card = if S.Paired w then 1 else 0

theorem Cslib.Circuits.Boolean.AffineDisperser.State.Valid.card_pairsMeeting_insert {n : ℕ} {f : BooleanFunction n} {S : State n} (hS : S.Valid f) {F : Finset ℕ} {x : ℕ} (hx : x ∉ F) (hpart : ∀ y ∈ F, ¬S.IsPartner x y) : (S.pairsMeeting (insert x F)).card = (S.pairsMeeting F).card + if S.Paired x then 1 else 0

Adding to F a parameter that is not the partner of a member of F adds its pair, if any.