A finite deck, two involutions, one survivor

The Windmill
Left Standing

Five integer windmills for 29 pair off under one rule, except one. Their oddness forces a different pairing to leave another standing, and that survivor reads 29 = 5² + 2². Then the same pairings become an algorithm.

29 is prime and 29 mod 4 = 1. The theorem applies.

The object

S₂₉, five positive integer windmills

Each card is a triple (x,y,z) satisfying x² + 4yz = 29. The centre has area x². Its four arms each have area yz. Nothing is sampled. The deck is the complete finite set.

Layer 1, pair the deck

One rule leaves one card

Press once. Zagier's map Z is self-inverse, so every moving card must have a partner. A fixed card has nowhere to go. Select any card to inspect its exact image.

Selected card under Zagier's map Select a card.
Selected card under the flip Select a card.

Layer 2, make the proof compute

Walk from one fixed point to the other

The parity proof promises a flip-fixed card but does not locate it. Start at the one known Z-fixed card. Each step applies flip first, then Z. The orbit is finite. Its other midpoint is fixed by the flip, where y = z.

Current orbit card (1,1,7)
1² + 4·1·7 = 29

An involution divides a finite set into two-card orbits and one-card fixed points. So the size of the set and the number of fixed points have the same oddness or evenness. Zagier's involution has exactly one fixed point on Sp, making the deck odd. The flip (x,y,z) ↦ (x,z,y) acts on the same deck, so it must also leave an odd number of cards fixed.

A flip-fixed card has y = z. Its printed invariant becomes p = x² + 4y² = x² + (2y)². That is the representation. For the algorithm, the finite orbit of the composition of the two involutions connects the known Z-fixed card to a flip-fixed card. The page prints every intermediate equality instead of asking you to trust the orbit.

The moat

The check

These counts are recomputed from the current input, in this browser, from positive integer enumeration. The offline verifier uses a different enumerator and compares the default result with published anchors before it trusts the page's rules.

External anchor for 29: Chan's published table lists the same five triples, and the published orbit figure takes two combined steps from (1,1,7) to (5,1,1). This engine recomputes both before comparing them. Run node research/zagier-involution/verify-zagier-involution.mjs.

Uncertainty and assumptions

  • The finite arithmetic has no numerical uncertainty within the stated cap. It uses exact safe integers.
  • Primality is load-bearing. A composite congruent to 1 modulo 4 is labelled exploration, and the proof algorithm is disabled.
  • The strict boundaries x = y-z and x = 2y have no branch. Qualifying prime decks avoid them. Other inputs report them.
  • The claims about HOL4 and Coq are reports from the cited papers. Their proof-assistant scripts are not executed by this page or its Node verifier.

Free choices and vacuous settings

  • You choose the input. The cap 9999, lexicographic card order, colours, and drawing scale are presentation choices.
  • Preset values are assigned exactly in JavaScript. No stepped slider quantises a published input.
  • The convention reports the positive odd-even pair. Signs and order give equivalent representations.
  • Starting on a flip-fixed card makes a zero-step display. It is named as vacuous and is not used as evidence for the constructive layer.
What is proved, and what is merely explored

The theorem mode is limited to primes p ≡ 1 (mod 4). There the page enumerates the full set, checks closure and both involution laws, counts the fixed points, runs the alternating orbit, and compares its result with a separate brute-force search for two squares.

Composite values such as 25 may still build an interesting deck, but the unique-fixed-point claim can fail and a strict branch boundary can appear. The page keeps that failure visible. No performance claim is made for the alternating algorithm, and no comparison with Cornacchia's algorithm is attempted.

Sources checked field by field
  1. D. Zagier, "A One-Sentence Proof That Every Prime p Congruent to 1 mod 4 Is a Sum of Two Squares", The American Mathematical Monthly 97(2), February 1990, page 144, DOI 10.2307/2323918. The scan contains the strict three-branch map, the sole fixed point, the parity argument, and the note that the proof is not constructive.
  2. Hing Lun Chan, "Windmills of the minds: an algorithm for Fermat's Two Squares Theorem", CPP 2022, pages 251 to 264, DOI 10.1145/3497775.3503673. The arXiv record was submitted 5 December 2021 and revised 14 January 2022, with exactly two versions. It supplies the alternating algorithm and its HOL4 correctness proof.
  3. Guillaume Dubach and Fabian Muehlboeck, "Formal verification of Zagier's one-sentence proof", arXiv preprint. The record was submitted 21 March 2021 and revised 24 April 2021, with exactly two versions and no journal reference. It reports proofs written with Mathematical Components in Coq.