An upper bound from a single injection — do two lines on paper stay short in Lean?

When lattice edges are chosen so that every plaquette (unit square) contains at most one, how many edges can be chosen?

The same material as 03. There we confirmed by finite decision that a family with "exactly one" exists. Here we relax the condition to "at most one" and derive an upper limit on how many can be chosen. The tool for the limit is just one thing — an injection.

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.

A chosen edge can be represented as a pair "direction μ and starting point x". To this pair we assign the starting point x alone.

If two edges left the same starting point x in two directions μ ≠ ν, those 2 edges would be 2 edges of the same plaquette (x; μ, ν). A plaquette contains at most one, so this does not happen. Hence the assignment is injective, and the number of chosen edges is at most the number of vertices.

The total number of edges is "number of directions × number of vertices", so in terms of density this means at most 1/d. Two lines on paper. Whether a short proof stays short in Lean is what this page wants to see.

Write it without fixing the vertex type

The paper proof uses almost nothing about the "lattice". All it uses is that there is a map "advance one step in direction i". So it was written with the vertex type left as X and the one-step map left as sh.

This way the same lemma applies to both the periodic lattice (ZMod L)^d and the infinite lattice ℤ^d. If the vertex type were fixed as ZMod L, the same proof would have to be written again for the ℤ^d version. Look at what the proof uses, and take out of the type what it does not use — that is the move for not writing things twice.

Do not say "matching"

While thinking on paper, one wants to say "the chosen edges form a matching (no two share a vertex)". On the whole lattice this is false. The 2 edges (μ, x) and (μ, x + e_μ) lined up in the same direction share the vertex x + e_μ, but they never lie on a common plaquette, so they can be chained as far as you like.

What can be said is "at each vertex, at most one edge in the positive direction", and that is enough for the bound. To confirm this distinction, an actually chained example is put into Lean.

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

theorem Line_atMostOne : AtMostOne Line := by decide

/--
**`I` is not a matching**: `Line` has two edges sharing a vertex (`(0, x)` and `(0, x+e_0)`, lined up in a row).
This is exactly why the paper proof said "cut into unit cubes, then a matching".
-/
theorem Line_not_matching : ∃ x : Wp 2 4, Line 0 x = true ∧ Line 0 (shiftp x 0) = true := by
  decide

LeanPlaquettePacking.Line_atMostOne · PlaquettePacking.Line_not_matching. A family that satisfies "at most one" and is not a matching really exists, so it is the paper's wording that gets corrected.

Build the edge set with a Finset filter

As in 03, the family is a Bool-valued function I. To count edges it has to be turned into a Finset, so we filter the whole of Fin d × vertex by the condition.

/-- The edge set of `I` (a subset of `Fin d × vertex`). -/
def edgeSet [NeZero L] (I : Fin d → Wp d L → Bool) : Finset (Fin d × Wp d L) :=
  Finset.univ.filter (fun p => I p.1 p.2 = true)

[NeZero L] is the hypothesis "L is not 0". ZMod 0 is ℤ itself and not finite, so without it Finset.univ cannot be formed. A hypothesis attached on the type side — the sort of condition one does not write on paper.

/--
`Packing sh I`: on a lattice with vertex type `X` and a map `sh` that "advances one step in direction `i`",
the family of edges `I : Fin d → X → Bool` (`I μ x` is the edge from `x` to `sh x μ`)
**contains at most one edge in every plaquette**.

The 4 edges of plaquette `(x; μ, ν)` are `(μ, x)`, `(μ, sh x ν)`, `(ν, x)`, `(ν, sh x μ)`.
-/
def Packing (sh : X → Fin d → X) (I : Fin d → X → Bool) : Prop :=
  ∀ μ ν : Fin d, μ ≠ ν → ∀ x : X,
    (I μ x).toNat + (I μ (sh x ν)).toNat + (I ν x).toNat + (I ν (sh x μ)).toNat ≤ 1

The two lines on paper become three lemmas, just as they are.

/-- **Core (one direction only)**: edges of `I` never leave one vertex in two directions. -/
theorem not_two_dirs {sh : X → Fin d → X} {I : Fin d → X → Bool} (h : Packing sh I)
    {μ ν : Fin d} (hμν : μ ≠ ν) {x : X} (hμ : I μ x = true) (hν : I ν x = true) : False

/-- The map `(μ, x) ↦ x` is injective on the edge set of `I`. -/
theorem snd_injOn {sh : X → Fin d → X} {I : Fin d → X → Bool} (h : Packing sh I)
    {p q : Fin d × X} (hp : I p.1 p.2 = true) (hq : I q.1 q.2 = true) (hpq : p.2 = q.2) :
    p = q := by
  by_cases hd : p.1 = q.1
  · exact Prod.ext hd hpq
  · exact absurd (not_two_dirs h hd hp (hpq ▸ hq)) id

Brought down to the periodic lattice, the number of vertices can be written L^d.

/--
**Main theorem**: a family with at most one edge in every plaquette has at most `L^d` edges, the number of vertices.
-/
theorem card_edgeSet_le [NeZero L] {I : Fin d → Wp d L → Bool} (h : AtMostOne I) :
    (edgeSet I).card ≤ L ^ d := by
  have := card_le_card_vertices (X := Wp d L) (sh := shiftp) h
  rwa [card_Wp] at this

LeanPlaquettePacking.not_two_dirs · snd_injOn · card_le_card_vertices · card_edgeSet_le. There is also a version that does not assume periodicity — in the form: the edges leaving a finite box S number at most |S|.

/--
**Box version**: if the edges of a packing `J` on `ℤ^d` leave only from vertices of a finite set `S`,
then there are at most `|S|` such edges. (`S` may be a box or anything else. Periodicity is not assumed.)
-/
theorem card_le_of_support [DecidableEq (Wz d)] {J : Fin d → Wz d → Bool} (h : AtMostOneZ J)
    (S : Finset (Wz d)) (T : Finset (Fin d × Wz d))
    (hT : ∀ p ∈ T, J p.1 p.2 = true ∧ p.2 ∈ S) : T.card ≤ S.card

The core lemma

theorem not_two_dirs {sh : X → Fin d → X} {I : Fin d → X → Bool} (h : Packing sh I)
    {μ ν : Fin d} (hμν : μ ≠ ν) {x : X} (hμ : I μ x = true) (hν : I ν x = true) : False := by
  have hle := h μ ν hμν x
  rw [hμ, hν] at hle
  simp only [Bool.toNat_true] at hle
  omega

Four lines. What they do.

• have hle := h μ ν hμν x — Apply the hypothesis "every plaquette has at most one" to the pair of directions (μ, ν) and the base point x. This gives us the inequality (I μ x).toNat + (I μ (sh x ν)).toNat + (I ν x).toNat + (I ν (sh x μ)).toNat ≤ 1.
• rw [hμ, hν] at hle — From the hypotheses we know I μ x = true and I ν x = true, so rewrite those two places to true.
• simp only [Bool.toNat_true] at hle — Turn true.toNat into 1. The inequality takes the form 1 + a + 1 + b ≤ 1.
• omega — A tactic that solves linear arithmetic over the natural numbers. 1 + a + 1 + b ≤ 1 cannot hold in the natural numbers, so a contradiction (False) comes out.

These four lines correspond to the paper's "because they are 2 edges of the same plaquette". On paper it is a phrase; in Lean it is four steps: apply the hypothesis, plug in the values, tidy the shape, crush it with arithmetic. What grew is only the number of moves; nothing more had to be thought.

From the injection to the cardinality

theorem card_le_card_vertices [Fintype X] [DecidableEq X] {sh : X → Fin d → X}
    {I : Fin d → X → Bool} (h : Packing sh I) :
    (Finset.univ.filter (fun p : Fin d × X => I p.1 p.2 = true)).card ≤ Fintype.card X := by
  classical
  rw [← Finset.card_univ (α := X)]
  refine Finset.card_le_card_of_injOn (fun p => p.2) (fun p _ => Finset.mem_univ _) ?_
  intro p hp q hq hpq
  simp only [Finset.coe_filter, Finset.mem_univ, true_and, Set.mem_ofPred_eq] at hp hq
  exact snd_injOn h hp hq hpq

• classical — Lets us split cases without worrying about decidability. This is a claim about an upper bound, so it need not be in computable form.
• rw [← Finset.card_univ …] — Rewrite the right side, "the number of elements of type X", as "the cardinality of the whole set of X". This brings both sides to Finset cardinalities.
• Finset.card_le_card_of_injOn — This is the core. The mathlib lemma "if a map from a set A to B is injective on A, then |A| ≤ |B|"; we pass it three things: the map (fun p => p.2), the fact that its values land in B, and injectivity.
• intro … / simp only … / exact snd_injOn … — Hand the remaining injectivity proof to the lemma built above. The simp only line just turns membership in Finset.filter back into "the predicate is true".

Seven lines. Against one line on paper, the only thing added was the procedure of "aligning to the language of cardinalities". No reindexing of sums as in the count is needed, so this stays short.

Put this page's bound (number of edges ≤ number of vertices) next to the counting identity of 04 (for a family with "exactly one", 4·(number of edges) = d·L^d), and the dimension is fixed.

/-- **Main theorem (two lines)**: if a perfect family exists on the periodic lattice, then `d ≤ 4`. -/
theorem perfect_torus_d_le_four [NeZero L] {I : Fin d → Wp d L → Bool} (h : PerfectP I) :
    d ≤ 4 := by
  rcases Nat.lt_or_ge d 2 with hd | hd
  · omega
  have h1 : 4 * (edgeSet I).card = d * L ^ d := four_mul_card_eq h hd
  have h2 : (edgeSet I).card ≤ L ^ d := card_edgeSet_le (perfectP_atMostOne h)
  have hL : 0 < L ^ d := pow_pos (Nat.pos_of_ne_zero (NeZero.ne L)) d
  have h3 : d * L ^ d ≤ 4 * L ^ d := by
    rw [← h1]
    exact Nat.mul_le_mul_left 4 h2
  exact Nat.le_of_mul_le_mul_right h3 hL

LeanPlaquetteCounting.perfect_torus_d_le_four. The body really is two lines. Just divide d·L^d = 4·|I| ≤ 4·L^d by L^d > 0; in the case d ≤ 1 the conclusion is trivial, and omega takes care of it.

How the two bounds share the territory can also be seen in numbers. This page's bound is density 1/d; the bound of 04 is density 1/4; at d = 4 they coincide exactly. At d = 3, L = 2 the bound 6 from 04 is stronger than the vertex bound 8; at d = 5, L = 2 it is the 1/d side that bites. Both are in Lean, together with the families that attain them.

LeanAll machine-checked. That a bound exists and that the bound is attained are different claims. The attainment side writes down a concrete family and confirms it with decide (the same procedure as in 03).

"There is no 'exactly one' family in 5 or more dimensions" is in Lean by another road too, completely different from the one above. Looking only at the concluding sentence they seem the same, but the statements differ. Side by side:

/-- **Theorem (lattice version)**: `ℤ^d` with `d ≥ 5` has no perfect family (periodicity not assumed). -/
theorem no_perfectZ_of_five {d : ℕ} (hd : 5 ≤ d) (J : Fin d → W d → Bool) : ¬ PerfectZ J :=
  fun hJ => no_perfect_of_five hd _ (restrict_perfect hJ)

LeanPerfectFamily.no_perfectZ_of_five. Neither contains the other. The torus version excludes only "families of period L", so it says nothing about families with no period. The lattice version assumes no periodicity, but the road is long: it puts the finite decision of 03 at the core and goes through a minimum-distance argument, "an edge in direction μ is the same edge if its position agrees outside 2 coordinates".

Even with the same concluding sentence, different hypotheses and types make a different theorem. To avoid citing one while talking about the other, a table like this is made first. How to read a statement itself is in How to read a statement.

lake env lean PlaquetteCounting.lean

864 lines, 0 errors, 0 warnings, about 9 seconds. The axiom output looks like this.

'PlaquettePacking.not_two_dirs' depends on axioms: [propext, Quot.sound]
'PlaquettePacking.snd_injOn' depends on axioms: [propext, Quot.sound]
'PlaquettePacking.card_le_card_vertices' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquettePacking.card_edgeSet_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PlaquettePacking.Line_not_matching' depends on axioms: [propext, Classical.choice, Quot.sound]

The thing to notice is that Classical.choice does not appear for the two core lemmas (not_two_dirs · snd_injOn). For these two we can read off that the axiom of choice is not used. From the cardinality lemma onward we wrote classical, so it appears. Both are within the three standard axioms; no sorryAx and no Lean.ofReduceBool.

Something to confirm on the short-proof side. The four-line lemma ends with omega, but omega adds no axioms. It is a decision procedure for linear arithmetic over the natural numbers and the integers, and the proof it produces is assembled inside Lean. The worry that a strong tactic might add axioms is answered directly by #print axioms.

What card_edgeSet_le says is this.

If a family I on the lattice (ZMod L)^d of period L satisfies "every plaquette has at most one", then the number of "pairs of a direction and a starting point" chosen by I is at most L^d.

Three things it does not say.

• It does not say "this bound is attained". Attainment is a separate claim: at d = 4, 5 there are families that attain it (bound_tight_d4 · bound_tight_d5), and at d = 3 it is not attained. An upper-bound theorem says only "nothing above here"; it does not say "this is reached".
• What the "edge set" counts is "pairs of a direction and a starting point". It does not count lattice edges as geometric objects; it counts the elements of a subset of Fin d × vertex. That the two correspond one-to-one follows from normalizing to the positive direction, but it is not part of the statement itself.
• It says nothing about families without a period. When that is needed, it is card_le_of_support (the box version) or no_perfectZ_of_five (the lattice version).

The second is the debt most easily overlooked in this kind of formalization. Whether the set being counted is in one-to-one correspondence with the objects one wanted to count lies outside the cardinality theorem. Continued in It compiles — but does it say what you meant?

Sources and reproduction

Next: 06 Series and inequalities — leaving finite combinatorics for infinite sums. Terms are in 12 Glossary.