Writing a count with Finset — what comes out when a double count is carried across

If lattice edges are chosen so that every plaquette (unit square) contains exactly one, what fraction of all edges is chosen?

In 03 we confirmed that such a choice exists in 4 dimensions, and in 05 we see that with "at most one" the number of edges is at most the number of vertices. Here we compute the ratio. The answer is exactly 1/4, independent of the dimension and of the size of the period.

The tool is double counting — counting the same thing two ways to get an equation, the most basic move in combinatorics. What happens when that basic move is carried into Lean is the content of this page. It is the combinatorics that comes up when estimating strong-coupling constants in lattice field theory; there is no claim here about the continuum limit or the mass gap, the actual Millennium Problem.

What we count are pairs (a chosen edge e, a plaquette p containing e).

Counting from the plaquette side. Every plaquette contains exactly one, so the number of pairs equals the number of plaquettes. There are d(d−1)/2 pairs of directions and L^d base points, so the number of plaquettes is d(d−1)L^d/2.

Counting from the edge side. An edge with direction μ and starting point x lies, for each choice of another direction ν ≠ μ, in 2 plaquettes in that direction (the one based at x and the one based at x − e_ν). There are d−1 choices of ν, so 2(d−1) plaquettes for each 1 edge. The number of pairs is 2(d−1)|I|.

Setting the two equal and simplifying, we get this.

On paper it is 5 lines. When carried into Lean, the snags are two spots in those 5 lines: the "d−1" and the "2 plaquettes".

Make the vertices Fin d → ZMod L

Since we take sums, the vertices must be finite. ZMod L is the type of "remainders on division by L", and Fin d → ZMod L is the torus of period L. The reason for choosing it is that the translation x ↦ x + e_ν is a bijection. In a finite box, a translation walks off the boundary, and the count fills up with boundary corrections.

Count plaquettes by "ordered pair and base point"

On paper we counted plaquettes by "an unordered pair of directions {μ, ν} and a base point", which produced the factor d(d−1)/2. In Lean we count by an ordered pair (μ, ν) (μ ≠ ν) and a base point. Each plaquette is then counted 2 times, but both sides are multiplied by the same 2, so the conclusion does not change.

What we gain is symmetry. Written with unordered pairs, we would range over the subsets of Finset (Fin d) of cardinality 2, and every rearrangement of a sum would bring a case split on "which one is μ". With ordered pairs it is simply ∑ μ, ∑ ν ∈ univ.erase μ — "for every μ, for every ν other than μ".

Give the count inside a plaquette a name

The main character of the count is "how many edges are in one plaquette", so we make that a definition.

/-- The number of the 4 edges of plaquette `(x; μ, ν)` that lie in `I`. -/
def plaqCount (I : Fin d → Wp d L → Bool) (μ ν : Fin d) (x : Wp d L) : ℕ :=
  (I μ x).toNat + (I μ (shiftp x ν)).toNat + (I ν x).toNat + (I ν (shiftp x μ)).toNat

/-- The number of edges in direction `μ`. -/
def dirCount [NeZero L] (I : Fin d → Wp d L → Bool) (μ : Fin d) : ℕ :=
  ∑ x : Wp d L, (I μ x).toNat

With these, the hypotheses can be restated in a readable form. Only the names change, so the proof is Iff.rfl (the same by definition).

theorem atMostOne_iff_plaqCount (I : Fin d → Wp d L → Bool) :
    AtMostOne I ↔ ∀ μ ν : Fin d, μ ≠ ν → ∀ x : Wp d L, plaqCount I μ ν x ≤ 1 := Iff.rfl

theorem perfectP_iff_plaqCount (I : Fin d → Wp d L → Bool) :
    PerfectP I ↔ ∀ μ ν : Fin d, μ ≠ ν → ∀ x : Wp d L, plaqCount I μ ν x = 1 := Iff.rfl

LeanPlaquetteCounting.plaqCount · dirCount · atMostOne_iff_plaqCount · perfectP_iff_plaqCount. A lemma whose proof is Iff.rfl exists for the reader alone. It lets the later proofs be read without having to check that "the hypothesis AtMostOne I means plaqCount ≤ 1", which makes it worth writing down.

Writing the paper proof's 2(d−1)|I| directly in natural numbers is dangerous. Natural-number subtraction stops at 0.

/-- Natural-number subtraction stops at 0. -/
example : (2 : ℕ) - 3 = 0 := by decide

This is not a defect of Lean; it is the convention that makes subtraction a total function on the natural-number type. The trouble is that an expression written d − 1 silently becomes 0 when d = 0, and the equation you want to prove can end up "true but empty". Moving to the integers would settle it, but cardinalities are natural numbers, so every move adds a coercion.

The move taken here is to rewrite the statement into a form with no subtraction in it. Not S = 4(d−1)N but S + 4N = 4dN.

/-- **Identity (main)**: summing the number of edges of `I` inside a plaquette over ordered pairs `(μ,ν)` and base points `x`
gives `4(d−1)|I|` (in the subtraction-free form `S + 4|I| = 4d|I|`). **No hypothesis on `I` is needed.** -/
theorem sum_plaqCount_add [NeZero L] (I : Fin d → Wp d L → Bool) :
    (∑ μ : Fin d, ∑ ν ∈ Finset.univ.erase μ, ∑ x : Wp d L, plaqCount I μ ν x)
      + 4 * (edgeSet I).card = 4 * d * (edgeSet I).card

In this form the statement is correct for d = 0 and d = 1 as well, and it loses none of its meaning (both sides just become 0). The step that extracts |I| from the equation is split off as an arithmetic lemma.

/-- Auxiliary (natural-number arithmetic): if `S + u = n·u` and `S + v = n·v` then `u = v` (`n ≥ 2`). -/
theorem eq_of_add_eq_mul {S u v n : ℕ} (hn : 2 ≤ n) (hu : S + u = n * u) (hv : S + v = n * v) :
    u = v

/-- Auxiliary (natural-number arithmetic): if `S + u = n·u`, `W + v = n·v` and `S ≤ W` then `u ≤ v` (`n ≥ 2`). -/
theorem le_of_add_eq_mul {S W u v n : ℕ} (hn : 2 ≤ n) (hu : S + u = n * u) (hv : W + v = n * v)
    (hSW : S ≤ W) : u ≤ v

LeanPlaquetteCounting.sum_plaqCount_add · eq_of_add_eq_mul · le_of_add_eq_mul. The hypothesis n ≥ 2 has gathered here. The paper's "divide by d−1" shows up in Lean as an arithmetic lemma that assumes d ≥ 2. Where d ≥ 2 was used can be read off from the hypothesis list without reading the proof.

The other snag in the paper proof is "2 plaquettes for each 1 edge". On a lattice of period L = 2, x + e_ν and x − e_ν are the same point, so one has to suspect that the "2" has in fact collapsed to 1.

The answer is that it does not collapse. But the reason is not "because the 2 are distinct" — it is that the count never goes through the number of plaquettes. Instead of counting plaquettes per edge, the Lean proof rewrites the sum side by a translation.

/-- `x ↦ x + e_ν` is a bijection on `(ZMod L)^d` (the inverse is `x ↦ x − e_ν`). -/
theorem shiftp_bijective [NeZero L] (ν : Fin d) :
    Function.Bijective (fun x : Wp d L => shiftp x ν)

/-- Reindexing under translation: `∑_x f(x + e_ν) = ∑_x f(x)`. -/
theorem sum_shiftp [NeZero L] (f : Wp d L → ℕ) (ν : Fin d) :
    ∑ x : Wp d L, f (shiftp x ν) = ∑ x : Wp d L, f x :=
  Fintype.sum_bijective _ (shiftp_bijective ν) _ _ (fun _ => rfl)

All that is used is "x ↦ x + e_ν is a bijection". No condition on the size of L is needed. At L = 2 the translation is an involution (doing it twice brings you back), but it is still a bijection, so the reindexing of the sum goes through just the same.

This is not a road chosen for Lean's convenience; it is the result of closing a hole in the paper proof. Saying "each edge lies in 2(d−1) plaquettes" tacitly uses that those plaquettes are distinct. Rewritten as a reindexing of a sum, that tacit assumption is no longer needed.

/-- **Recounting the slots**: summing the 4 slots of one plaquette over all `x` gives `2·(direction μ) + 2·(direction ν)`.
Only the translation bijection is used, so the same holds at `L = 2`. -/
theorem sum_x_plaqCount [NeZero L] (I : Fin d → Wp d L → Bool) (μ ν : Fin d) :
    ∑ x : Wp d L, plaqCount I μ ν x = 2 * dirCount I μ + 2 * dirCount I ν

/-- **(2) Upper bound from counting**: if every plaquette has at most one, then `4|I| ≤ d·L^d` (density `≤ 1/4`). -/
theorem four_mul_card_le [NeZero L] {I : Fin d → Wp d L → Bool} (h : AtMostOne I) (hd : 2 ≤ d) :
    4 * (edgeSet I).card ≤ d * L ^ d

/-- **(1) A perfect family has density exactly `1/4`**: `4|I| = d·L^d`. -/
theorem four_mul_card_eq [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) (hd : 2 ≤ d) :
    4 * (edgeSet I).card = d * L ^ d

/-- **Corollary (divisibility condition)**: if a perfect family exists, then `4 ∣ d·L^d`. -/
theorem four_dvd_of_perfect [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) (hd : 2 ≤ d) :
    4 ∣ d * L ^ d

A rational-number form is included too. This is the statement that reads literally as "density exactly 1/4".

theorem density_eq_quarter [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) (hd : 2 ≤ d) :
    ((edgeSet I).card : ℚ) / ((d : ℚ) * (L : ℚ) ^ d) = 1 / 4

LeanPlaquetteCounting.sum_x_plaqCount · four_mul_card_le · four_mul_card_eq · four_dvd_of_perfect · density_eq_quarter. Both the natural-number form and the rational form are put down because the former is easier to use in later proofs and the latter conveys the meaning to the reader.

The divisibility condition is a by-product, but it works on its own. With d = 3 and L = 3, 4 ∤ 3·27 = 81, so there is no perfect family — a case that the d ≤ 4 of 05 does not rule out. Conversely, d = 5 and L = 2 satisfies 4 ∣ 160, so divisibility does not rule it out; it is ruled out on the d ≤ 4 side. Neither corollary contains the other.

Recounting the slots

theorem sum_x_plaqCount [NeZero L] (I : Fin d → Wp d L → Bool) (μ ν : Fin d) :
    ∑ x : Wp d L, plaqCount I μ ν x = 2 * dirCount I μ + 2 * dirCount I ν := by
  have h1 : (∑ x : Wp d L, (I μ (shiftp x ν)).toNat) = ∑ x : Wp d L, (I μ x).toNat :=
    sum_shiftp (fun y => (I μ y).toNat) ν
  have h2 : (∑ x : Wp d L, (I ν (shiftp x μ)).toNat) = ∑ x : Wp d L, (I ν x).toNat :=
    sum_shiftp (fun y => (I ν y).toNat) μ
  simp only [plaqCount, dirCount]
  rw [Finset.sum_add_distrib, Finset.sum_add_distrib, Finset.sum_add_distrib, h1, h2]
  ring

• have h1 … / have h2 … — First prepare the fact that the sum of a translated term equals the untranslated sum. Of the 4 slots, 2 involve a translation, so 2 of these are needed.
• simp only [plaqCount, dirCount] — Unfold the names back to their definitions. It is simp only rather than simp because extra tidying would change the shape, and the next rw would no longer match.
• rw [Finset.sum_add_distrib, …, h1, h2] — Split into 4 terms using "the sum of a sum is the sum of the sums", then rewrite 2 of them with h1 and h2. sum_add_distrib appears 3 times because splitting 4 terms takes 3 cuts.
• ring — Tidy up the remaining a + a + b + b = 2a + 2b.

The paper's "2 plaquettes for each 1 edge" has become "2 of the 4 terms are rewritten by a translation". Talk of counting plaquettes has become talk of sums, so the size of the period never appears.

The off-diagonal sum — collapsing it without producing d−1

The step that adds up the inside of ∑ μ, ∑ ν ≠ μ is the most laborious part of this proof. What does the work is Finset.sum_erase_add — the lemma "a sum with one point removed, plus that point, is the whole sum". Let us check a short form by hand.

/-- A sum with one point removed, plus that point, is the whole sum.
This lemma is why the `d` times form can be reached without writing `d − 1`. -/
example {n : ℕ} (A : Fin n → ℕ) (μ : Fin n) :
    (∑ _ν ∈ Finset.univ.erase μ, A μ) + A μ = n * A μ := by
  rw [Finset.sum_erase_add _ _ (Finset.mem_univ μ), Finset.sum_const, Finset.card_univ,
    Fintype.card_fin, smul_eq_mul]

• Finset.sum_erase_add _ _ (Finset.mem_univ μ) — Turn the left side into "a sum over everything". Here we pass the fact that μ belongs to the whole set (Finset.mem_univ μ).
• Finset.sum_const — A sum of a term that does not depend on ν is "count × term".
• Finset.card_univ · Fintype.card_fin — Turn the "count" into n.
• smul_eq_mul — Turn the scalar action (•) that Finset.sum_const produces into ordinary multiplication.

Five rewrites, and we have the d-times form without d − 1 ever appearing. The main lemma (sum_erase_two) uses this twice — once for the terms that do not depend on ν and once for the ν terms.

This does not go through with Finset.sum_comm (swapping the order of summation). In the off-diagonal sum the range of ν depends on μ, so a naive swap leaves a condition on the range behind. Bringing it to "remove one point, add one point" gets rid of the dependence on the range from the start.

We look at whether the identity really gives that value, in the smallest case. On the lattice with d = 2 and period 4, take the 4 edges in direction 0 with x 1 = 0 (a closed straight line). The value of the identity should be 4(d−1)|I| = 4 · 1 · 4 = 16.

import Mathlib

/-- Vertices of the periodic lattice `(ZMod L)^d`. -/
abbrev Wp (d L : ℕ) : Type := Fin d → ZMod L

/-- Advance the `i`-th coordinate by 1. -/
def shiftp {d L : ℕ} (x : Wp d L) (i : Fin d) : Wp d L := Function.update x i (x i + 1)

/-- The number of the 4 edges of plaquette `(x; μ, ν)` that lie in `I`. -/
def plaqCount {d L : ℕ} (I : Fin d → Wp d L → Bool) (μ ν : Fin d) (x : Wp d L) : ℕ :=
  (I μ x).toNat + (I μ (shiftp x ν)).toNat + (I ν x).toNat + (I ν (shiftp x μ)).toNat

/-- On the lattice with `d = 2` and period 4, the 4 edges in direction 0 with `x 1 = 0`. -/
def Line (μ : Fin 2) (x : Wp 2 4) : Bool := (μ == 0) && (x 1 == 0)

/-- There are 4 edges. -/
example : (Finset.univ.filter (fun p : Fin 2 × Wp 2 4 => Line p.1 p.2 = true)).card = 4 := by
  decide

/-- The value of the double count: `4(d−1)|I| = 4 · 1 · 4 = 16`. -/
example : (∑ μ : Fin 2, ∑ ν ∈ Finset.univ.erase μ, ∑ x : Wp 2 4, plaqCount Line μ ν x) = 16 := by
  decide

LeanChecked by hand; it went through. decide actually computes the sum and produces 16 (the same tool as in 03). After proving the identity, confirming its value by a different road (the kernel's computation) is the job of this one line. If the proof side and the computation side produce the same number, a slip in writing the statement is considerably narrowed down.

A positive control of the same shape is in the main file too (sum_plaq_Line). And one negative control. The family that takes every edge violates the upper bound — this confirms that "the hypothesis is doing work".

/-- Negative control: the family taking every edge (`d=2`, `L=4`) violates the bound.
`4·32 = 128 > 32 = 2·4^2` ⟹ the hypothesis `AtMostOne` is doing work. -/
theorem full_violates_bound :
    ¬ (4 * (edgeSet (fun (_ : Fin 2) (_ : Wp 2 4) => true)).card ≤ 2 * 4 ^ 2) := by
  decide

lake env lean PlaquetteCounting.lean

864 lines, 0 errors, 0 warnings, about 9 seconds. A few lines from the axiom output:

'PlaquetteCounting.shiftp_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.sum_shiftp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.eq_of_add_eq_mul' depends on axioms: [propext, Quot.sound]
'PlaquetteCounting.sum_plaqCount_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.four_mul_card_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquetteCounting.density_eq_quarter' depends on axioms: [propext, Classical.choice, Quot.sound]

All within the three standard axioms; no sorryAx and no Lean.ofReduceBool. The point to notice is that Classical.choice does not appear for the arithmetic lemma eq_of_add_eq_mul. The step "extract |I| from the equation", split off in §04, closes without the axiom of choice.

What four_mul_card_eq says is this.

If a family I on the lattice (ZMod L)^d of period L (d ≥ 2, L ≥ 1) satisfies "every plaquette has exactly one", then 4 · |I| = d · L^d.

Three things it does not say.

• It does not say "such a family exists". It is a conditional equation, and it holds correctly even in cases where no family satisfies the condition (for instance d = 5). Writing "the density is exactly 1/4" reads as if one exists, but the statement says "if one exists". That one exists is shown separately by the concrete example in 03.
• d ≥ 2 cannot be dropped. At d = 1 there is not a single plaquette, so the condition is vacuously true, every edge can be taken, and the equation fails. The 2 ≤ d in the hypothesis list is doing its work there.
• An "edge" is a "pair of a direction and a starting point". The same debt as in 05: we are counting elements of Finset (Fin d × vertex). That these correspond one-to-one with the lattice edges is not part of the statement.

The first is the easiest thing to misread in equations of this kind. A conditional equation is true even in cases where the condition is not met. Unless it is read together with existence, it looks as if it said something it does not. Continued in It compiles — but does it say what you meant?

Sources and reproduction

Next: 05 An upper bound from a single injection — the same material, closed without sums. Terms are in 12 Glossary.