Squares on the four-clock

A whole-number square sits at 0 or 1 on the four-hour clock — never at 2.

Start with a concrete example

Square the numbers 0,1,2,3 and divide the results by 4. The remainders are 0,1,0,1. This suggests a pattern; the proof must explain why it continues.

A small check: try the idea

Think with the concrete example above. You can try again.

What remainder does 5² leave after division by 4?

Read the answer and reasoning

1. 5²=25=4×6+1. Computing one example checks that example; the general square-remainder claim still needs its proof.

Build the idea in three steps

Put squares on a four-hour clock: 0 ^ 2 = 0, 1 ^ 2 = 1, 2 ^ 2 = 4 lands on 0, and 3 ^ 2 = 9 lands on 1. Whole-number squares only ever sit at 0 or 1 — the seat 2 stays empty.
The theorem sq_ne_two_fin_zmod_four says exactly that on the Lean clock type ZMod 4, and its proof is fin_cases plus decide: visit every position, check all four, done — a census, not a clever trick.
The integer version Int.sq_ne_two_mod_four transfers it to ordinary squares with remainders. This little census is a school-sized telescope: it will tell the exponent-four case which leg of a triangle must be even.

A small example

Try it: 5 ^ 2 = 25 = 6 × 4 + 1 leaves remainder 1, and 6 ^ 2 = 36 = 9 × 4 leaves remainder 0. No integer square leaves remainder 2 when divided by 4.

Lean definition · original excerpt

Mathlib · db584cd · PythagoreanTriples.lean

31theorem sq_ne_two_fin_zmod_four (z : ZMod 4) : z * z ≠ 2 := by32  change Fin 4 at z33  fin_cases z <;> decide34 35theorem Int.sq_ne_two_mod_four (z : ℤ) : z * z % 4 ≠ 2 := by36  suffices ¬z * z % (4 : ℕ) = 2 % (4 : ℕ) by exact this37  rw [← ZMod.intCast_eq_intCast_iff']38  simpa using sq_ne_two_fin_zmod_four _

How to read this Lean

On the four-clock, even numbers square to 0 because 2 · 2 = 4, while odd numbers square to 1 because odd × odd is always one past a multiple of 4 — twice something plus one, squared. The first proof checks a finite clock by brute force, the census a school table would make; the second lifts the fact into integer-remainder language by passing through the clock type once (rw [← ZMod.intCast_eq_intCast_iff']). Files often pay for a one-line fact like this with a small census of cases.

Original source ↗ · L31–38 Open the complete saved source

Where this idea is used

7. The veterans’ cabinet

Squares on the four-clock

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue