Handing a finite check to decide — confirming a choice of lattice edges in one word

On the 4-dimensional lattice, is there a choice of edges such that every small square contains exactly one of them?
(Lattice: the figure whose vertices are the points with integer coordinates, with an edge joining two points that differ by 1 in exactly one coordinate. Plaquette = small square: the unit square determined by two directions μ, ν and a base point x; it has 4 edges.)

This combinatorial question comes up when estimating a constant in the strong-coupling regime of a lattice field theory. Only the combinatorial part is treated here; there is no claim about the continuum limit or the mass gap — the actual Millennium problem.

To show "there is one", it is enough to construct one and show it, and whether the constructed formula really satisfies the condition is settled by examining every one of the finitely many plaquettes. A claim that is settled by examining every one of finitely many cases can be handed to Lean in the single word decide. On this page we look in turn at how to hand it over, what Lean says when you hand it over wrongly, and from what size it becomes heavy.

Call the 4 directions by the numbers 0, 1, 2, 3, and write the coordinates of a vertex as x 0, x 1, x 2, x 3. Looking only at the parity of each coordinate, there are 16 vertices, and we choose edges by the following 4 rules.

There are 24 plaquettes: 6 pairs of directions {μ, ν} times 4 parities of the remaining 2 coordinates. Confirm for each of the 24 that "exactly 1 of the 4 edges is chosen", and the proof is done; written on paper, it is a table of 24 rows. What the human does here is "confirm", not "think". So we hand it to the machine.

decide does not work unless the claim has the form "splits into finitely many cases, and in each case the truth is settled by computation". So at the definition stage we use only enumerable types and computable predicates. There are three choices.

Vertices as Fin d → Bool

The lattice itself is infinite. Here we look only at the parity of each coordinate, and take a vertex to be Fin d → Bool (a sequence of d truth values, i.e. a vertex of the unit d-cube). Fin d → Bool is a finite type with 2^d elements, and Lean knows how to enumerate it.

Taking vertices as Fin d → ℤ would be the lattice itself, but it is infinite, so the ∀ in "for every plaquette" does not close under decide. Taking residues ZMod L gives a finite periodic lattice, and that is the type used in counting. The Bool version, looking only at parity, corresponds to L = 2 and is the lightest.

The family of edges as a Bool-valued function

A set of edges could be written as a Set or a Finset, but here we made it I : Fin d → V d → Bool — a function that takes a direction and a position and returns "chosen or not" as a truth value. A Set is a predicate with no guarantee of being computable, and a Finset is a list without duplicates, so writing the family as a formula drags in extra proofs. With a function returning Bool, the definition of the family is itself the procedure for computing it.

An edge in direction μ is determined by "the values of the coordinates other than μ". Since x and "x with its μ coordinate flipped" are the same edge, we normalise to the side with x μ = false and write (μ, x).

"Exactly one" as a sum of toNat

Using toNat, which turns a Bool into 0 or 1, we write that the values of the 4 slots of a plaquette add up to 1. "Exactly one of the 4 edges" could also be written with the cardinality of a Finset, but with a sum the evaluation is nothing but addition.

This way of writing does, however, take on one debt. "The sum of the values of the 4 slots is 1" means "one of the 4 edges" only when the 4 slots point at distinct edges. That has to be proved separately, and in fact a lemma called face_slots_ne is included. When you make the writing lighter, what you made lighter comes out as a separate lemma — how to find debts of this kind is treated in It passed — but does it say what you meant?.

/-- A vertex of the unit `d`-cube. -/
abbrev V (d : ℕ) : Type := Fin d → Bool

/-- Flip the `i`-th coordinate (`x ↦ x + e_i`). -/
def flipAt (x : V d) (i : Fin d) : V d := Function.update x i (!x i)

/--
`I μ x`: the edge in direction `μ` at position `x` (normalised to `x μ = false`)
is in the family.

`Perfect I`: for every 2-dimensional face determined by `μ ≠ ν` and `z μ = z ν = false`,
exactly one of its 4 edges `(μ, z)`, `(μ, z+e_ν)`, `(ν, z)`, `(ν, z+e_μ)` is in `I`.
-/
def Perfect (I : Fin d → V d → Bool) : Prop :=
  ∀ μ ν : Fin d, μ ≠ ν → ∀ z : V d, z μ = false → z ν = false →
    (I μ z).toNat + (I μ (flipAt z ν)).toNat
      + (I ν z).toNat + (I ν (flipAt z μ)).toNat = 1

The 4 rules written on paper become formulas as they are.

/-- An example of a perfect family for `d = 4`. 2 edges per direction,
antipodal in the remaining 3 coordinates. -/
def I4 (μ : Fin 4) (x : V 4) : Bool :=
  if μ = 0 then ((x 1 == x 2) && !(x 2 == x 3))
  else if μ = 1 then ((x 2 == x 3) && !(x 3 == x 0))
  else if μ = 2 then ((x 0 == x 1) && (x 1 == x 3))
  else ((x 0 == x 2) && !(x 2 == x 1))

/-- A perfect family exists for `d = 4`. -/
theorem perfect_I4 : Perfect I4 := by decide

LeanPerfectFamily.perfect_I4. The proof is the single word by decide. There are examples for d = 3 and d = 2 as well (perfect_I3, perfect_I2), and for d ≤ 1 there is no 2-dimensional face, so every family satisfies the condition (perfect_of_le_one). Conversely, for d ≥ 5 there is none — that is treated in An upper bound from a single injection.

The decide above does not pass as it stands. Perfect is written as a def returning Prop, so Lean's instance search does not look inside it. Let us confirm this by hand. Check the following file.

import Mathlib

/-- The thing to be decided. Written as a `def` returning `Prop`. -/
def AtMostOne2 (I : Fin 2 → (Fin 2 → Bool) → Bool) : Prop :=
  ∀ μ ν : Fin 2, μ ≠ ν → ∀ z : Fin 2 → Bool, (I μ z).toNat + (I ν z).toNat ≤ 1

def J (μ : Fin 2) (x : Fin 2 → Bool) : Bool := if μ = 0 then !x 1 else false

theorem J_atMostOne : AtMostOne2 J := by decide

Lean says this.

error: failed to synthesize
  Decidable (AtMostOne2 J)

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

The reply is "I do not know that this claim is decidable". Everything inside AtMostOne2 (a ∀ over finite types and an inequality on natural numbers) is decidable, yet the search stops at the point where it is wrapped in the name of a def. The only fix is to add one instance that unfolds the name and then runs the search.

/-- Unfold the `def` and then run the instance search. -/
instance instDecidableAtMostOne2 (I : Fin 2 → (Fin 2 → Bool) → Bool) :
    Decidable (AtMostOne2 I) := by
  unfold AtMostOne2; infer_instance

Add this, and by decide passes. The original Perfect comes with a one-liner of the same shape.

instance instDecidablePerfect (I : Fin d → V d → Bool) : Decidable (Perfect I) := by
  unfold Perfect; infer_instance

The lesson is one line. If you are going to hand a predicate named with def … : Prop to decide, supply the decidability instance yourself. If you write it with abbrev, the inside is visible and no instance is needed, but in exchange the displayed statement gets longer.

One more thing to look at is the wording when decide says "I examined it, and it was false". Hand it ∀ b : Bool, b = true and you get the following.

error: Tactic `decide` proved that the proposition
  ∀ (b : Bool), b = true
is false

Read these two messages as distinct. The first is "there is no way to decide"; the second is "decided, and it was false". The first is a problem with how the definition is written, the second a problem with the claim itself, and the place to fix is different.

decide is not magic; it does the following three things in order.

1. Find the decision procedure. It assembles, by instance search, an instance of Decidable P for the claim P. A ∀ over a finite type becomes the procedure "list every element and examine them all", and an equation of natural numbers becomes "compute both sides and compare".
2. Run that procedure in the kernel. Lean's kernel (the smallest trusted part) evaluates the assembled procedure according to the definitions. For perfect_I4, it tries all 12 ordered pairs of directions × 16 positions, and confirms that the sum is 1 on the 24 plaquettes that satisfy the condition.
3. If the result is true, turn it into a proof. It applies the lemma (of_decide_eq_true) that obtains the original claim from "the decision procedure returned true".

The lemma at the core of this road is an exhaustive decision over 12 truth values.

/-- From "exactly one" on the 6 faces of a 3-dimensional sub-cube, exactly one of the
4 edges in direction `μ` is in the family. A finite decision over `2^12 = 4096` cases. -/
theorem cube3_bool : ∀ m00 m01 m10 m11 n00 n01 n10 n11 l00 l01 l10 l11 : Bool,
    m00.toNat + m10.toNat + n00.toNat + n10.toNat = 1 →
    m01.toNat + m11.toNat + n01.toNat + n11.toNat = 1 →
    m00.toNat + m01.toNat + l00.toNat + l10.toNat = 1 →
    m10.toNat + m11.toNat + l01.toNat + l11.toNat = 1 →
    n00.toNat + n01.toNat + l00.toNat + l01.toNat = 1 →
    n10.toNat + n11.toNat + l10.toNat + l11.toNat = 1 →
    m00.toNat + m01.toNat + m10.toNat + m11.toNat = 1 := by decide

LeanPerfectFamily.cube3_bool. The 6 hypotheses are the 6 faces of a 3-dimensional sub-cube; m is the 4 edges in direction μ, n the 4 edges in ν, l the 4 edges in lam. Insert one finite decision at the 3-dimensional level, and from there the proof proceeds for general dimension d. This is the clearest form of the division "reduce to finite and decide; do by hand what cannot be reduced".

4096 cases take an instant. So where does it become heavy? We measured the exhaustive decision over n truth values while varying n. The values have the baseline 5 seconds (loading import Mathlib) subtracted.

computationMeasured on this machine (4 cores, 15 GB RAM). With 20 variables, the following message appears.

error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.

Remove the cutoff with set_option maxHeartbeats 0 and it passes. The rule of thumb is "up to a hundred thousand cases, seconds; from a million, minutes".

But the number of cases alone does not decide it. For the same 2^n cases, if the form is not "∀ over n truth values" but "∀ over all functions Fin n → Bool", then on this machine n = 14 (16,384 cases) took about 2 minutes. The work of assembling a function is added to every case. When it is heavy, look first at "what is computed per case", not at the number of cases.

One more thing: you may hit the depth setting.

set_option maxRecDepth 100000

This is the limit on recursion depth, and hitting it prints "maximum recursion depth has been reached". This one is a matter of settings, not of computational cost, so raising it lets it pass. The time cutoff (heartbeats) and the depth cutoff (recDepth) are different things.

"It passed with by decide" is not, by itself, grounds for reassurance. We also confirm that a family with the condition broken comes out as "does not satisfy". If the failing side never appears, the suspicion remains that the condition was vacuously true (for example, that there was not a single plaquette to examine).

/-- Negative control: the empty family is not perfect (`d = 3`). -/
theorem not_perfect_empty3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => false) := by decide

/-- Negative control: the family of all edges is not perfect (`d = 3`). -/
theorem not_perfect_full3 : ¬ Perfect (fun (_ : Fin 3) (_ : V 3) => true) := by decide

/-- Negative control: replacing direction 0 of `I4` by "all" makes it
not perfect (`d = 4`). -/
theorem not_perfect_I4_broken :
    ¬ Perfect (fun (μ : Fin 4) (x : V 4) => if μ = 0 then true else I4 μ x) := by decide

LeanPerfectFamily.not_perfect_empty3, not_perfect_full3, not_perfect_I4_broken. The third is the one that matters. Breaking just one direction of a family that passed makes it fail, so the decision really is reading the contents of the family.

The check is nothing more than passing one file through Lean.

lake env lean PerfectFamily.lean

498 lines, 0 errors, 0 warnings, about 7 seconds. What the proofs rely on is printed as is by #print axioms.

#print axioms PerfectFamily.cube3_bool
#print axioms PerfectFamily.perfect_I4
#print axioms PerfectFamily.not_perfect_I4_broken

'PerfectFamily.cube3_bool' does not depend on any axioms
'PerfectFamily.perfect_I4' depends on axioms: [propext, Classical.choice, Quot.sound]
'PerfectFamily.not_perfect_I4_broken' depends on axioms: [propext, Classical.choice, Quot.sound]

Three points on reading this.

• propext, Classical.choice and Quot.sound are the three standard axioms of Lean and mathlib, and ordinary mathematics stands on them. That nothing other than these three appears is the point to confirm (What Lean is).
• cube3_bool uses no axioms at all. An exhaustive decision over truth values closes on the definitions of the computation alone. Classical.choice appears in perfect_I4 because assembling the enumeration of Fin d → Bool goes through mathlib's tools on the way; it has no bearing on the strength of the claim.
• There are two things that must not appear. sorryAx is an unproved hole (a place where sorry was written), and Lean.ofReduceBool is the trace of native_decide.

The "7 min 11 s" in the table above would be an instant with native_decide, but that compiles the decision procedure to machine code, runs it, and trusts the result of the run. Since the place where trust sits moves from the kernel to the compiler and the runtime environment, we do not use it here (01). The other options when speed falls short are in What is realistically too heavy for Lean.

What perfect_I4 : Perfect I4 says is the following.

For the choice of edges determined by the formula I4, on every 2-dimensional face of the unit 4-cube, exactly one of the face's 4 slots is chosen.

Three things it does not say.

• It does not say "on the whole lattice". The type of vertices is Fin 4 → Bool, not Fin 4 → ℤ. Whether the family obtained by extending I4 with period 2 satisfies the condition on the whole lattice is a different statement on a different type (PerfectZ, which assumes no periodicity). That is in Lean too, but it is not the same theorem — the differences are laid out in 05.
• It does not say "there is no other". This is a claim of existence, not a classification of families.
• That the "4 slots" are "4 distinct edges" lies outside this statement. It is the debt taken on the moment we wrote it as a sum of toNat, and a separate lemma face_slots_ne pays it back. Without that lemma, this theorem is the computational fact "the sum is 1", not the geometric fact "exactly one edge".

The third is the kind of hole most easily missed in a machine check. decide answers correctly about the formula you wrote, but does not answer whether the formula you wrote was what you meant. Continue to It passed — but does it say what you meant?.

Sources and reproduction

Next: 04 Counting with Finset — counting "how many can be chosen" on the same subject. Terms are in 12 Glossary.