From b2d4edaa2ed16c00167feb18751567c9f9671e2e Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 20 Oct 2024 00:13:18 +0200
Subject: [PATCH 1/6] ch4 second proof, latex and widget

---
 FormalBook/Chapter_04.lean          | 235 ++++++++++++++++++++++++++++
 FormalBook/Widgets/Windmill.lean    | 145 +++++++++++++++++
 blueprint/src/chapter/chapter04.tex | 192 +++++++++++++++++++++--
 3 files changed, 560 insertions(+), 12 deletions(-)
 create mode 100644 FormalBook/Widgets/Windmill.lean

diff --git a/FormalBook/Chapter_04.lean b/FormalBook/Chapter_04.lean
index f8ce083..c7809d7 100644
--- a/FormalBook/Chapter_04.lean
+++ b/FormalBook/Chapter_04.lean
@@ -16,6 +16,8 @@ limitations under the License.
 Authors: Moritz Firsching
 -/
 import Mathlib.Tactic
+import FormalBook.Widgets.Windmill
+
 /-!
 # Representing numbers as sums of two squares
 
@@ -45,3 +47,236 @@ import Mathlib.Tactic
 -/
 
 
+namespace ch04
+
+open Nat
+
+lemma lemma₁ {p : ℕ} [h : Fact p.Prime] :
+    let num_solutions := Finset.card { s : ZMod p | s ^ 2 = - 1 }
+    (∃ m, p = 4 * m + 1 → num_solutions = 2) ∧
+    (p = 2 → num_solutions = 1) ∧
+    (∃ m, p = 4 * m + 1 → num_solutions = 0) := by
+  constructor
+  · sorry
+  · constructor
+    · intro hp
+      -- TODO: figure out how to easily write `use 1` here to follow more closely the book
+      aesop
+    · sorry
+
+-- TODO: golf, and perhaps make it even close to book proof
+lemma lemma₂ (n m : ℕ) (hn : n = 4 * m + 3) :
+  ¬ ∃ a b, n = a ^2 + b ^2 := by
+  push_neg
+  intro a b
+  by_contra h
+  have : (n : ZMod 4) =  a ^ 2 + b ^ 2 := by
+    rw [h]
+    simp only [Nat.cast_add, Nat.cast_pow]
+  rw [hn] at this
+  simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] at this
+  rw [mul_eq_zero_of_left (by rfl) (m : ZMod 4), zero_add] at this
+  have hx : ∀ (x : ZMod 4),  x ^2 ∈ ({0, 1} : Finset (ZMod 4)) := by
+    intro x
+    fin_cases x <;> simp
+    · left
+      rfl
+    · right
+      rfl
+  have ha := hx <| a
+  have hb := hx  <| b
+  generalize hA: (a : ZMod 4) ^ 2 = A
+  generalize hB: (b : ZMod 4) ^ 2 = B
+  rw [hA, hB] at this
+  rw [hA] at ha
+  rw [hB] at hb
+  fin_cases A <;> fin_cases B <;> norm_num at this <;> tauto
+
+-- We follow a similar path taken by Jeremy Tan and Thomas Browning in
+-- mathlib4/Archive/ZagierTwoSquares.lean.
+
+theorem theorem₁  {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) : ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by
+  sorry
+
+section Sets
+
+open Set
+
+variable (k : ℕ) [hk : Fact (4 * k + 1).Prime]
+
+/-- We study the set S -/
+def S : Set (ℤ × ℤ × ℤ) := {((x, y, z) : ℤ × ℤ × ℤ) | 4 * x * y + z ^ 2 = 4 * k + 1 ∧ x > 0 ∧ y > 0}
+
+noncomputable instance : Fintype (S k) := by
+  sorry
+
+end Sets
+
+section Involutions
+
+open Function
+
+variable (k : ℕ)
+
+/- 1. -/
+
+/-- The linear involution `(x, y, z) ↦ (y, x, -z)`. -/
+def linearInvo : Function.End (S k) := fun ⟨⟨x, y, z⟩, h⟩ => ⟨⟨y, x, -z⟩, by
+  simp only [S, Set.mem_setOf_eq] at h ⊢
+  exact ⟨by linarith [h], h.2.2, h.2.1⟩ ⟩
+
+theorem linearInvo_sq : linearInvo k ^2  = (1 : Function.End (S k)) := by
+  change linearInvo k ∘ linearInvo k = id
+  funext x
+  simp only [linearInvo, comp_apply, neg_neg, Prod.mk.eta, Subtype.coe_eta]
+  rfl
+
+theorem linearInvo_no_fixedPoints : IsEmpty (fixedPoints (linearInvo k)) := by
+  simp
+  intro x y z h
+  intro hfixed
+  simp only [IsFixedPt, linearInvo, Subtype.mk.injEq, Prod.mk.injEq] at hfixed
+  have : z = 0 := by linarith
+  obtain ⟨h, _, _⟩ := h
+  simp only [this, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero] at h
+  apply_fun (· % 4) at h
+  simp [mul_assoc, Int.add_emod] at h
+
+def T : Set (ℤ × ℤ × ℤ) := {((x, y, z) : ℤ × ℤ × ℤ) | (x,y,z) ∈ S k ∧ z > 0}
+
+noncomputable instance : Fintype <| T k := by
+  sorry
+
+def U : Set (ℤ × ℤ × ℤ) := {((x, y, z) : ℤ × ℤ × ℤ) | (x,y,z) ∈ S k ∧ (x - y) + z > 0}
+
+noncomputable instance : Fintype <| U k := by
+  sorry
+
+theorem sameCard : Fintype.card (U k) = Fintype.card (T k) := by
+  sorry
+
+/- 2. -/
+
+/-- The second involution that we study is an involution on the set U. -/
+def secondInvo : Function.End (U k) := fun ⟨⟨x, y, z⟩, h⟩ =>
+  ⟨⟨x - y + z, y, 2 * y - z⟩, by
+  obtain ⟨hS, h⟩ := h
+  simp [U]
+  simp [S] at *
+  constructor
+  · constructor
+    · rw [← hS.1]
+      ring_nf
+    constructor
+    · exact h
+    · exact hS.2.2
+  linarith⟩
+
+/-- `complexInvo k` is indeed an involution. -/
+theorem secondInvo_sq : secondInvo k ^ 2 = 1 := by
+  change secondInvo k ∘ secondInvo k = id
+  funext ⟨⟨x, y, z⟩, h⟩
+  rw [comp_apply]
+  simp [secondInvo]
+  ring
+
+variable [hk : Fact (4 * k + 1).Prime]
+theorem k_pos : 0 < k := by
+  by_contra h
+  simp at h
+  rw [h] at hk
+  simp at hk
+  tauto
+
+
+
+/-- The singleton containing `(1, 1, k)`. -/
+def singletonFixedPoint : Finset (U k) :=
+  {⟨(k, 1, 1), ⟨by
+    simp [S]
+    exact k_pos k,
+    by
+    simp
+    exact k_pos k⟩⟩}
+
+/-- Any fixed point of `complexInvo k` must be `(1, 1, k)`. -/
+theorem eq_of_mem_fixedPoints : fixedPoints (secondInvo k) = singletonFixedPoint k := by
+  simp only [fixedPoints, IsFixedPt, secondInvo, singletonFixedPoint, Prod.mk_one_one,
+    Finset.coe_singleton]
+  ext t
+  constructor
+  · intro ht
+    simp at ht
+    sorry
+  · aesop
+
+/-- `complexInvo k` has exactly one fixed point. -/
+theorem card_fixedPoints_eq_one : Fintype.card (fixedPoints (secondInvo k)) = 1 := by
+  simp only [eq_of_mem_fixedPoints, singletonFixedPoint]
+  rfl
+
+theorem card_T_odd : Odd <| Fintype.card <| T k := by
+  sorry
+
+/- 3. -/
+/- The third, trivial, involution `(x, y, z) ↦ (x, z, y)`. -/
+def trivialInvo : Function.End (T k) := fun ⟨⟨x, y, z⟩, h⟩ => ⟨⟨y, x, z⟩, by
+  simp [T, S] at *
+  obtain ⟨⟨h, hx, hy⟩, hz⟩ := h
+  exact ⟨⟨by
+    rw [← h]
+    ring, hy, hx⟩, hz⟩
+  ⟩
+
+/-- If `trivialInvo k` has a fixed point, a representation of `4 * k + 1` as a sum of two squares
+can be extracted from it. -/
+theorem sq_add_sq_of_nonempty_fixedPoints (hn : (fixedPoints (trivialInvo k)).Nonempty) :
+    ∃ a b : ℤ, a ^ 2 + b ^ 2 = 4 * k + 1 := by
+  simp only [sq]
+  obtain ⟨⟨⟨x, y, z⟩, he⟩, hf⟩ := hn
+  have := mem_fixedPoints_iff.mp hf
+  simp only [trivialInvo, Subtype.mk.injEq, Prod.mk.injEq, true_and] at this
+  simp only [T, S, Set.mem_setOf_eq] at he
+  simp [IsFixedPt, trivialInvo] at hf
+  use (2 * y), z
+  rw [show 2 * y * (2 * y) = 4 * y * y by linarith, ← he.1.1]
+  rw [hf.2]
+  ring
+
+theorem trivialInvo_fixedPoints : (fixedPoints (trivialInvo k)).Nonempty := by sorry
+
+end Involutions
+
+theorem theorem₂ {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) :
+    ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by
+  rw [← div_add_mod p 4, hp] at h ⊢
+  let k := p / 4
+  have ⟨a, b, h⟩ := sq_add_sq_of_nonempty_fixedPoints k <| trivialInvo_fixedPoints k
+  use a.natAbs
+  use b.natAbs
+  unfold k at h
+  zify
+  simpa only [sq_abs] using h
+
+
+
+-- The windged sqaure of area 4xy + z^2 = 73 that corresponds to (x,y,z) = (3,4,5)
+
+def xyz := ((4, 3, 5) : ℤ × ℤ × ℤ)
+
+def toTriple := fun (xyz : ℤ × ℤ × ℤ) ↦
+    (some <|  {x := xyz.1.natAbs, y := xyz.2.1.natAbs, z := xyz.2.2.natAbs} : Option WindmillTriple)
+
+#widget WindmillWidget with { triple? :=(toTriple xyz) : WindmillWidgetProps }
+
+-- ... and its winged shape
+
+#widget WindmillWidget with ({ triple? := (toTriple xyz), colors? := greyColors} : WindmillWidgetProps)
+
+-- The second winged derived from the windeg shape of are 73 using `secondInvo`:
+
+def secondInvo_of_xyz := (((ch04.secondInvo 18) ⟨xyz, sorry⟩).1)
+
+#eval! secondInvo_of_xyz
+
+#widget WindmillWidget with ({triple? := (toTriple secondInvo_of_xyz)} : WindmillWidgetProps)
diff --git a/FormalBook/Widgets/Windmill.lean b/FormalBook/Widgets/Windmill.lean
new file mode 100644
index 0000000..0d1b5e2
--- /dev/null
+++ b/FormalBook/Widgets/Windmill.lean
@@ -0,0 +1,145 @@
+
+import Lean.Util.Paths
+import LeanSearchClient.Syntax
+import ProofWidgets.Component.Basic
+
+
+/-! ## Example use of string diagram widgets -/
+structure WindmillTriple where
+  x : Nat
+  y : Nat
+  z : Nat
+deriving DecidableEq, Repr, Inhabited,  Lean.ToJson, Lean.FromJson
+
+structure WindmillColors where
+  square? : Option String := some "grey"
+  north?: Option String := "'#a1c4fd'"
+  east? : Option String := "'#fda1c4'"
+  south?: Option String := "'#fddca1'"
+  west? : Option String := "'#c4fda1'"
+deriving DecidableEq, Repr, Inhabited,  Lean.ToJson, Lean.FromJson
+
+structure WindmillWidgetProps where
+  triple? : Option WindmillTriple := none
+  colors? : Option WindmillColors := some default
+  deriving Lean.Server.RpcEncodable
+
+open ProofWidgets
+
+@[widget_module]
+def WindmillWidget : Component WindmillWidgetProps where
+  javascript := "
+    import { InteractiveCode } from '@leanprover/infoview'
+    import * as React from 'react'
+
+    export default function(props) {
+      const WindmillPattern = () => {
+        const subSquareSize = 20;
+
+        // Extract the values from props
+        const z = props.triple.z || 5;
+        const x = props.triple.x || 2;
+        const y = props.triple.y || 3;
+
+        // Use colors from props
+        const colors = props.colors || {};
+        const squareColor = colors.square || 'lightgray';
+        const northColor = colors.north || '#a1c4fd'; // Default to light blue if not provided
+        const eastColor = colors.east || '#fda1c4';  // Default to light pink
+        const southColor = colors.south || '#fddca1'; // Default to light orange
+        const westColor = colors.west || '#c4fda1';  // Default to light green
+
+        const squareSize = z * subSquareSize;
+        const rectWidth = y * subSquareSize;
+        const rectHeight = x * subSquareSize;
+        const startX = 120;
+        const startY = 120;
+
+        // Create SVG for the central square and the four rectangles
+        const createSquares = () => {
+          const elements = [];
+
+          // Central square
+          for (let row = 0; row < z; row++) {
+            for (let col = 0; col < z; col++) {
+              const xPos = startX + col * subSquareSize;
+              const yPos = startY + row * subSquareSize;
+              elements.push(
+                React.createElement('rect', {
+                  x: xPos, y: yPos, width: subSquareSize, height: subSquareSize,
+                  fill: squareColor, stroke: 'white', strokeWidth: 0.5
+                })
+              );
+            }
+          }
+
+          // Four rectangles with colors from props
+          const rectanglePositions = [
+            { x: startX, y: startY - rectHeight, rows: x, cols: y, fill: northColor }, // Top (North)
+            { x: startX + squareSize, y: startY, rows: y, cols: x, fill: eastColor },  // Right (East)
+            { x: startX + squareSize - rectWidth, y: startY + squareSize, rows: x, cols: y, fill: southColor }, // Bottom (South)
+            { x: startX - rectHeight, y: startY + squareSize - rectWidth, rows: y, cols: x, fill: westColor }  // Left (West)
+          ];
+
+          rectanglePositions.forEach(pos => {
+            for (let row = 0; row < pos.rows; row++) {
+              for (let col = 0; col < pos.cols; col++) {
+                const xPos = pos.x + col * subSquareSize;
+                const yPos = pos.y + row * subSquareSize;
+                elements.push(
+                  React.createElement('rect', {
+                    x: xPos, y: yPos, width: subSquareSize, height: subSquareSize,
+                    fill: pos.fill, stroke: 'white', strokeWidth: 0.5
+                  })
+                );
+              }
+            }
+          });
+
+          return elements;
+        };
+
+        return React.createElement('svg', {
+          width: '100%',
+          height: '100%',
+          viewBox: '0 0 400 400',  // Adjust based on your SVG dimensions
+          style: { display: 'block', margin: '0 auto' } // Center horizontally
+        }, createSquares());
+      };
+
+      return React.createElement('div', {
+        style: {
+          display: 'flex',
+          justifyContent: 'center',
+          alignItems: 'center',
+          height: '100%',
+          textAlign: 'center'
+        }
+      }, React.createElement(WindmillPattern));
+    }"
+
+
+#widget WindmillWidget with { triple? := some <| {x := 2, y :=7, z := 3} : WindmillWidgetProps }
+
+#widget WindmillWidget with { triple? := some <| {x := 5, y := 5, z := 3} : WindmillWidgetProps }
+
+#widget WindmillWidget with { triple? := some <| {x := 3, y := 7, z := 2} : WindmillWidgetProps }
+
+def greyColors := ( some <| {
+    square? := some "lightgrey",
+    north? := some "lightgrey",
+    east? := some "lightgrey",
+    south? := some "lightgrey",
+    west? := some "lightgrey"
+  } : Option WindmillColors)
+
+#widget WindmillWidget with ({
+  triple? := some <| {x := 3, y := 7, z := 2},
+  colors? := some <| {
+    square? := some "lightgrey",
+    north? := some "lightgrey",
+    east? := some "lightgrey",
+    south? := some "lightgrey",
+    west? := some "lightgrey"
+  }
+} : WindmillWidgetProps)
diff --git a/blueprint/src/chapter/chapter04.tex b/blueprint/src/chapter/chapter04.tex
index b1a203d..a773ba1 100644
--- a/blueprint/src/chapter/chapter04.tex
+++ b/blueprint/src/chapter/chapter04.tex
@@ -1,50 +1,218 @@
 \chapter{Representing numbers as sums of two squares}
 
 \begin{lemma}[Lemma 1]
-  \label{ch3.lemma1}
+  \lean{ch4.lemma₁}
+  \label{ch4.lemma1}
   For primes \(p = 4m + 1\) the equation \(s^2 \equiv -1 (\mod p)\) has two
   solutions \(s \in \{1, 2, \dots, p - 1\}\), for \(p = 2\) there is one such solution, while
   for primes of the form \(p = 4m + 3\) there is no solution.
 \end{lemma}
 \begin{proof}
-  TODO
+   For $p = 2$ take $s = 1$.
+   For odd $p$, we construct the equivalence relation on
+   $\{1, 2, \dots, p - 1\}$ that is generated by identifying every
+   element with its additive inverse and with its multiplicative inverse
+   in $\mathbb{Z}_p$. Thus the ``general'' equivalence classes will contain four elements
+  \[
+  \{x, -x, \overline{x}, -\overline{x}\}
+  \]
+since such a 4-element set contains both inverses for all its elements. However,
+there are smaller equivalence classes if some of the four numbers are not distinct:
+
+\begin{itemize}
+  \item $x \equiv -x$ is impossible for odd $p$.
+  \item $x \equiv \overline{x}$ is equivalent to $x^2 \equiv 1$. This has two solutions,
+    namely $x = 1$ and $x = p - 1$, leading to the equivalence class $\{1, p - 1\}$ of size 2.
+  \item $x \equiv -\overline{x}$ is equivalent to $x^2 \equiv -1$. This equation may
+    have no solution or two distinct solutions $x_0, p - x_0$: in this case the equivalence
+    class is $\{x_0, p - x_0\}$.
+\end{itemize}
+
+The set $\{1, 2, \dots, p - 1\}$ has $p - 1$ elements, and we have partitioned it
+into quadruples (equivalence classes of size 4), plus one or two pairs (equivalence
+classes of size 2). For $p - 1 = 4m + 2$ we find that there is only the one pair $\{1, p - 1\}$,
+the rest is quadruples, and thus $s^2 \equiv -1 \pmod{p}$ has no solution.
+For $p - 1 = 4m$ there has to be the second pair,
+and this contains the two solutions of $s^2 \equiv -1$ that we were looking for.
 \end{proof}
 
 
 \begin{lemma}[Lemma 2]
-  \label{ch3.lemma2}
+  \label{ch4.lemma2}
+  \lean{ch4.lemma₂}
   No number \(n = 4m + 3\) is a sum of two squares.
 \end{lemma}
 \begin{proof}
-  TODO
+  \leanok
+  The square of any even number is $(2k)^2 = 4k^2 \equiv 0 \pmod{4}$,
+  while squares of odd numbers yield $(2k + 1)^2 = 4(k^2 + k) + 1 \equiv 1 \pmod{4}$.
+  Thus any sum of two squares is congruent to $0$, $1$ or $2 \pmod{4}$. \qed
 \end{proof}
 
 \begin{proposition}[First proof]
-  \label{ch3.proposition1}
+  \label{ch4.proposition1}
+  \lean{ch4.theorem₁}
   Every prime of the form \(p = 4m + 1\) is a sum of two squares,
   that is, it can be written as \(p = x^2 + y^2\) for some natural numbers \(x,y \in \mathbb{N}\).
 \end{proposition}
 \begin{proof}
-  \uses{ch3.lemma1}
-  TODO
+  \uses{ch4.lemma1}
+  Consider the pairs $(x', y')$ of integers with $0 \leq x', y' \leq \sqrt{p}$, that is,
+  $x', y' \in \{0, 1, \dots, \lfloor \sqrt{p} \rfloor\}$.
+  There are $(\lfloor \sqrt{p} \rfloor + 1)^2$ such pairs.
+  Using the estimate $\lfloor x \rfloor + 1 > x$ for $x = \sqrt{p}$, we see that we have more
+  than $p$ such pairs of integers. Thus for any $s \in \mathbb{Z}$, it is impossible that all
+  the values $x' - sy'$ produced by the pairs $(x', y')$ are distinct modulo $p$. That is, for
+  every $s$ there are two distinct pairs
+  \[
+  (x', y'), (x'', y'') \in \{0, 1, \dots, \lfloor \sqrt{p} \rfloor\}^2
+  \]
+  with $x' - sy' \equiv x'' - sy'' \pmod{p}$. Now we take differences:
+  We have $x' - x'' \equiv s(y' - y'') \pmod{p}$. Thus if we define
+  $x := |x' - x''|$, $y := |y' - y''|$, then we get
+  \[
+  (x, y) \in
+  \{0, 1, \dots, \lfloor \sqrt{p} \rfloor\}^2 \quad \text{with} \quad x \equiv \pm sy \pmod{p}.
+  \]
+  Also we know that not both $x$ and $y$ can be zero, because the pairs $(x', y')$ and $(x'', y'')$
+  are distinct.
+
+  Now let $s$ be a solution of $s^2 \equiv -1 \pmod{p}$, which exists by Lemma 1.
+  Then $x^2 \equiv s^2 y^2 = -y^2 \pmod{p}$, and so we have produced
+  \[
+  (x, y) \in
+  \mathbb{Z}^2 \quad \text{with} \quad
+  0 < x^2 + y^2 < 2p \quad \text{and} \quad x^2 + y^2 \equiv 0 \pmod{p}.
+  \]
+  But $p$ is the only number between $0$ and $2p$ that is divisible by $p$.
+  Thus $x^2 + y^2 = p$: done!
 \end{proof}
 
 \begin{proposition}[Second proof]
-  \label{ch3.proposition2}
+  \label{ch4.proposition2}
+  \lean{ch4.theorem₂}
   Every prime of the form \(p = 4m + 1\) is a sum of two squares,
   that is, it can be written as \(p = x^2 + y^2\) for some natural numbers \(x,y \in \mathbb{N}\).
 \end{proposition}
 \begin{proof}
-  TODO (Zagier's one line proof is in mathlib by now, follow this!)
+  \leanok
+ We study the set
+\[
+S := \{(x, y, z) \in \mathbb{Z}^3 : 4xy + z^2 = p, \ x > 0, \ y > 0\}.
+\]
+This set is finite. Indeed, $x \geq 1$ and $y \geq 1$ implies $y \leq \frac{p}{4}$ and
+$x \leq \frac{p}{4}$. So there are only finitely many possible values for $x$ and $y$, and given
+$x$ and $y$, there are at most two values for $z$.
+
+\begin{enumerate}
+    \item The first linear involution is given by
+    \[
+    f : S \to S, \quad (x, y, z) \mapsto (y, x, -z),
+    \]
+    that is, ``interchange $x$ and $y$, and negate $z$.'' This clearly maps $S$ to itself, and it is
+    an \emph{involution}: Applied twice, it yields the identity. Also, $f$ has no fixed points,
+    since $z = 0$ would imply $p = 4xy$, which is impossible. Furthermore, $f$ maps the solutions in
+    \[
+    T := \{(x, y, z) \in S : z > 0\}
+    \]
+    to the solutions in $S \setminus T$, which satisfy $z < 0$. Also, $f$ reverses the signs of
+    $x - y$ and of $z$, so it maps the solutions in
+    \[
+    U := \{(x, y, z) \in S : (x - y) + z > 0\}
+    \]
+    to the solutions in $S \setminus U$. For this we have to see that there is no solution with
+    $(x - y) + z = 0$, but there is none since this would give
+    $p = 4xy + z^2 = 4xy + (x - y)^2 = (x + y)^2$.
+
+    What do we get from the study of $f$? The main observation is that since $f$ maps the sets $T$
+    and $U$ to their complements, it also interchanges the elements in $T \setminus U$ with these in
+    $U \setminus T$. That is, there is the same number of solutions in $U$ that are not in $T$ as
+    there are solutions in $T$ that are not in $U$ — so $T$ and $U$ have the same cardinality.
+
+    \item The second involution that we study is an involution on the set $U$:
+    \[
+    g : U \to U, \quad (x, y, z) \mapsto (x - y + z, y, 2y - z).
+    \]
+    First we check that indeed this is a well-defined map: If $(x, y, z) \in U$, then
+    $x - y + z > 0$, $y > 0$ and $4(x - y + z)y + (2y - z)^2 = 4xy + z^2$, so $g(x, y, z) \in S$.
+    By $(x - y + z) - y + (2y - z) = x > 0$ we find that indeed $g(x, y, z) \in U$.
+
+    Also $g$ is an involution: $g(x, y, z) = (x - y + z, y, 2y - z)$ is mapped by $g$ to
+    $((x - y + z) - y + (2y - z), y, 2y - (2y - z)) = (x, y, z)$.
+
+    And finally $g$ has exactly one fixed point:
+    \[
+    (x, y, z) = g(x, y, z) = (x - y + z, y, 2y - z)
+    \]
+    implies that $y = z$, but then $p = 4xy + y^2 = (4x + y)y$, which holds only for $y = z = 1$ and
+    $x = \frac{p - 1}{4}$.
+
+    But if $g$ is an involution on $U$ that has exactly one fixed point, then
+    \emph{the cardinality of $U$ is odd.}
+
+    \item The third, trivial, involution that we study is the involution on $T$ that interchanges
+    $x$ and $y$:
+    \[
+    h : T \to T, \quad (x, y, z) \mapsto (y, x, z).
+    \]
+    This map is clearly well-defined, and an involution. We combine now our knowledge derived from
+    the other two involutions: The cardinality of $T$ is equal to the cardinality of $U$, which is
+    odd. But if $h$ is an involution on a finite set of odd cardinality, then
+    \emph{it has a fixed point}: There is a point $(x, y, z) \in T$ with $x = y$, that is,
+    a solution of
+    \[
+    p = 4x^2 + z^2 = (2x)^2 + z^2.
+    \]
+\end{enumerate}
+
 \end{proof}
 
 \begin{proposition}[Third proof]
-  \label{ch3.proposition3}
+  \label{ch4.proposition3}
   Every prime of the form \(p = 4m + 1\) is a sum of two squares,
   that is, it can be written as \(p = x^2 + y^2\) for some natural numbers \(x,y \in \mathbb{N}\).
 \end{proposition}
 \begin{proof}
-  TODO
+    Again we fix a prime number $p = 4n + 1$ and consider the set of solutions
+\[
+T = \{(x, y, z) \in \mathbb{N}^3 : 4xy + z^2 = p\}.
+\]
+Each element of this set gives rise to a \emph{winged square}: This is the figure consisting of a
+square and four rectangles in the plane that you get if you start with a square of side length $z$
+and at each vertex attach a rectangle of side-lengths $x$ and $y$ in a rotation-symmetric way,
+such that the edge of length $x$ points away from the square, while the edge of length $y$ runs
+along the side of the square.
+
+We consider two winged squares ``the same'' if they are congruent. One way to make this unique,
+such that the representation of the winged square depends only on its boundary curve, is to require
+that the L formed by the two edges in the upper right-hand corner is at least as high as it is wide.
+If this condition is not satisfied, then a mirror image (reflected, e.g., in a vertical axis), will
+repair this. So each solution in $T$ corresponds to a \emph{unique} winged square of area
+$4xy + z^2 = p$, and indeed this is reversible: From each winged square we can read off a solution.
+
+Taking the union of the square and the four rectangles, we get for each winged square what we will
+call a \emph{unique winged shape}: This is a polyomino of area $p$ with four-fold rotation symmetry,
+ which has twelve vertices: eight convex ones with inner right angle and four non-convex ones with
+ outer right angle.
+ (We can't get a square shape, since $p$ is a prime, so it can't be a square number.)
+ Again we will consider winged shapes ``the same'' if they are congruent, so we might assume that
+ the L shape in the upper right-hand corner is at least as high as it is wide.
+
+ Now we are getting very close to the punch line: For each winged shape we get
+ \emph{either one or two} winged squares, by simultaneously drawing, in a rotation-symmetric way,
+ vertical and horizontal lines to the interior starting at the non-convex vertices. We get
+ \emph{only one} solution if the shape has the symmetry of a square, that is, if the two arms of the
+ L shapes have the same length. This happens exactly if $y = z$, but then
+ $p = 4xz + z^2 = (4x + z)z$; assuming that $p$ is a prime, this implies that $z = 1$ and $x = n$.
+ In other words: Exactly one winged shape yields a single winged square, while all other winged
+ shapes yield two winged squares each.
+ Consequently, \emph{the number $|T|$ of winged squares is odd.}
+
+However, the winged squares with non-square rectangles (with $x \neq y$) come in pairs, as we can
+always flip the four rectangular wings between vertical and horizontal format
+(that is, exchange $x$ and $y$). As $|T|$ is odd, this implies that there is an odd number of winged
+squares whose wings are squares, that is, $T$ contains an odd number of triples $(x, y, z)$
+with $x = y$, and hence at least one, and this yields a solution to $(2x)^2 + z^2 = p$.
 \end{proof}
 
 \begin{theorem}
@@ -54,6 +222,6 @@ \chapter{Representing numbers as sums of two squares}
   even exponent in the prime decomposition of \(n\).
 \end{theorem}
 \begin{proof}
-  \uses{ch3.lemma2, ch3.proposition1, ch3.proposition2, ch3.proposition3}
+  \uses{ch4.lemma2, ch4.proposition1, ch4.proposition2, ch4.proposition3}
   TODO
 \end{proof}

From 2993757d7c4c4796827d97c04cebda4758ce0fa7 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 20 Oct 2024 12:30:19 +0200
Subject: [PATCH 2/6] fix build

---
 blueprint/lean_decls                |  6 +++++-
 blueprint/src/chapter/chapter04.tex | 22 +++++++++++-----------
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index 1823ed0..16adbab 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -11,6 +11,10 @@ chapter2.bound_factorial
 chapter2.bound_binomial_coeff
 chapter3.sylvester
 chapter3.binomials_coefficients_never_powers
+ch04.lemma₁
+ch04.lemma₂
+ch04.theorem₁
+ch04.theorem₂
 book.quadratic_reciprocity.fermat_little
 book.quadratic_reciprocity.euler_criterion
 book.quadratic_reciprocity.product_rule
@@ -42,4 +46,4 @@ fundamental_theorem_of_algebra
 pigeon_hole_principle
 chapter44.friendship_theorem
 chapter45.theorem_1
-ramsey_exists
\ No newline at end of file
+chapter45.ramsey_exists
\ No newline at end of file
diff --git a/blueprint/src/chapter/chapter04.tex b/blueprint/src/chapter/chapter04.tex
index a773ba1..34a5866 100644
--- a/blueprint/src/chapter/chapter04.tex
+++ b/blueprint/src/chapter/chapter04.tex
@@ -1,8 +1,8 @@
 \chapter{Representing numbers as sums of two squares}
 
 \begin{lemma}[Lemma 1]
-  \lean{ch4.lemma₁}
-  \label{ch4.lemma1}
+  \lean{ch04.lemma₁}
+  \label{ch04.lemma1}
   For primes \(p = 4m + 1\) the equation \(s^2 \equiv -1 (\mod p)\) has two
   solutions \(s \in \{1, 2, \dots, p - 1\}\), for \(p = 2\) there is one such solution, while
   for primes of the form \(p = 4m + 3\) there is no solution.
@@ -38,8 +38,8 @@ \chapter{Representing numbers as sums of two squares}
 
 
 \begin{lemma}[Lemma 2]
-  \label{ch4.lemma2}
-  \lean{ch4.lemma₂}
+  \label{ch04.lemma2}
+  \lean{ch04.lemma₂}
   No number \(n = 4m + 3\) is a sum of two squares.
 \end{lemma}
 \begin{proof}
@@ -50,13 +50,13 @@ \chapter{Representing numbers as sums of two squares}
 \end{proof}
 
 \begin{proposition}[First proof]
-  \label{ch4.proposition1}
-  \lean{ch4.theorem₁}
+  \label{ch04.proposition1}
+  \lean{ch04.theorem₁}
   Every prime of the form \(p = 4m + 1\) is a sum of two squares,
   that is, it can be written as \(p = x^2 + y^2\) for some natural numbers \(x,y \in \mathbb{N}\).
 \end{proposition}
 \begin{proof}
-  \uses{ch4.lemma1}
+  \uses{ch04.lemma1}
   Consider the pairs $(x', y')$ of integers with $0 \leq x', y' \leq \sqrt{p}$, that is,
   $x', y' \in \{0, 1, \dots, \lfloor \sqrt{p} \rfloor\}$.
   There are $(\lfloor \sqrt{p} \rfloor + 1)^2$ such pairs.
@@ -89,8 +89,8 @@ \chapter{Representing numbers as sums of two squares}
 \end{proof}
 
 \begin{proposition}[Second proof]
-  \label{ch4.proposition2}
-  \lean{ch4.theorem₂}
+  \label{ch04.proposition2}
+  \lean{ch04.theorem₂}
   Every prime of the form \(p = 4m + 1\) is a sum of two squares,
   that is, it can be written as \(p = x^2 + y^2\) for some natural numbers \(x,y \in \mathbb{N}\).
 \end{proposition}
@@ -168,7 +168,7 @@ \chapter{Representing numbers as sums of two squares}
 \end{proof}
 
 \begin{proposition}[Third proof]
-  \label{ch4.proposition3}
+  \label{ch04.proposition3}
   Every prime of the form \(p = 4m + 1\) is a sum of two squares,
   that is, it can be written as \(p = x^2 + y^2\) for some natural numbers \(x,y \in \mathbb{N}\).
 \end{proposition}
@@ -222,6 +222,6 @@ \chapter{Representing numbers as sums of two squares}
   even exponent in the prime decomposition of \(n\).
 \end{theorem}
 \begin{proof}
-  \uses{ch4.lemma2, ch4.proposition1, ch4.proposition2, ch4.proposition3}
+  \uses{ch04.lemma2, ch04.proposition1, ch04.proposition2, ch04.proposition3}
   TODO
 \end{proof}

From 7c5aa525e373d81afac8c501f289b48b742858dd Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 20 Oct 2024 13:14:54 +0200
Subject: [PATCH 3/6] introduce secondInvo_fun

---
 FormalBook/Chapter_04.lean       | 19 ++++++++++---------
 FormalBook/Widgets/Windmill.lean | 21 +++++++--------------
 2 files changed, 17 insertions(+), 23 deletions(-)

diff --git a/FormalBook/Chapter_04.lean b/FormalBook/Chapter_04.lean
index c7809d7..ffb85d8 100644
--- a/FormalBook/Chapter_04.lean
+++ b/FormalBook/Chapter_04.lean
@@ -157,12 +157,14 @@ theorem sameCard : Fintype.card (U k) = Fintype.card (T k) := by
 
 /- 2. -/
 
+def secondInvo_fun := fun ((x,y,z) : ℤ × ℤ × ℤ) ↦ (x - y + z, y, 2 * y - z)
+
 /-- The second involution that we study is an involution on the set U. -/
 def secondInvo : Function.End (U k) := fun ⟨⟨x, y, z⟩, h⟩ =>
-  ⟨⟨x - y + z, y, 2 * y - z⟩, by
+  ⟨secondInvo_fun (x, y, z), by
   obtain ⟨hS, h⟩ := h
   simp [U]
-  simp [S] at *
+  simp [S, secondInvo_fun] at *
   constructor
   · constructor
     · rw [← hS.1]
@@ -177,7 +179,8 @@ theorem secondInvo_sq : secondInvo k ^ 2 = 1 := by
   change secondInvo k ∘ secondInvo k = id
   funext ⟨⟨x, y, z⟩, h⟩
   rw [comp_apply]
-  simp [secondInvo]
+  simp only [secondInvo, secondInvo_fun, sub_sub_cancel, id_eq, Subtype.mk.injEq, Prod.mk.injEq,
+    and_true]
   ring
 
 variable [hk : Fact (4 * k + 1).Prime]
@@ -201,8 +204,8 @@ def singletonFixedPoint : Finset (U k) :=
 
 /-- Any fixed point of `complexInvo k` must be `(1, 1, k)`. -/
 theorem eq_of_mem_fixedPoints : fixedPoints (secondInvo k) = singletonFixedPoint k := by
-  simp only [fixedPoints, IsFixedPt, secondInvo, singletonFixedPoint, Prod.mk_one_one,
-    Finset.coe_singleton]
+  simp only [fixedPoints, IsFixedPt, secondInvo, secondInvo_fun,
+    singletonFixedPoint, Prod.mk_one_one, Finset.coe_singleton]
   ext t
   constructor
   · intro ht
@@ -275,8 +278,6 @@ def toTriple := fun (xyz : ℤ × ℤ × ℤ) ↦
 
 -- The second winged derived from the windeg shape of are 73 using `secondInvo`:
 
-def secondInvo_of_xyz := (((ch04.secondInvo 18) ⟨xyz, sorry⟩).1)
-
-#eval! secondInvo_of_xyz
+#eval secondInvo_fun xyz
 
-#widget WindmillWidget with ({triple? := (toTriple secondInvo_of_xyz)} : WindmillWidgetProps)
+#widget WindmillWidget with ({triple? := (toTriple <| secondInvo_fun xyz)} : WindmillWidgetProps)
diff --git a/FormalBook/Widgets/Windmill.lean b/FormalBook/Widgets/Windmill.lean
index 0d1b5e2..f338a23 100644
--- a/FormalBook/Widgets/Windmill.lean
+++ b/FormalBook/Widgets/Windmill.lean
@@ -118,13 +118,6 @@ def WindmillWidget : Component WindmillWidgetProps where
       }, React.createElement(WindmillPattern));
     }"
 
-
-#widget WindmillWidget with { triple? := some <| {x := 2, y :=7, z := 3} : WindmillWidgetProps }
-
-#widget WindmillWidget with { triple? := some <| {x := 5, y := 5, z := 3} : WindmillWidgetProps }
-
-#widget WindmillWidget with { triple? := some <| {x := 3, y := 7, z := 2} : WindmillWidgetProps }
-
 def greyColors := ( some <| {
     square? := some "lightgrey",
     north? := some "lightgrey",
@@ -133,13 +126,13 @@ def greyColors := ( some <| {
     west? := some "lightgrey"
   } : Option WindmillColors)
 
+#widget WindmillWidget with { triple? := some <| {x := 2, y :=7, z := 3} : WindmillWidgetProps }
+
+#widget WindmillWidget with { triple? := some <| {x := 5, y := 5, z := 3} : WindmillWidgetProps }
+
+#widget WindmillWidget with { triple? := some <| {x := 3, y := 7, z := 2} : WindmillWidgetProps }
+
 #widget WindmillWidget with ({
   triple? := some <| {x := 3, y := 7, z := 2},
-  colors? := some <| {
-    square? := some "lightgrey",
-    north? := some "lightgrey",
-    east? := some "lightgrey",
-    south? := some "lightgrey",
-    west? := some "lightgrey"
-  }
+  colors? := greyColors
 } : WindmillWidgetProps)

From 501bf9205326e63816f0a44cb188050217ba119b Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 20 Oct 2024 13:46:16 +0200
Subject: [PATCH 4/6] center windmill

---
 FormalBook/Widgets/Windmill.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/FormalBook/Widgets/Windmill.lean b/FormalBook/Widgets/Windmill.lean
index f338a23..1b3fe6d 100644
--- a/FormalBook/Widgets/Windmill.lean
+++ b/FormalBook/Widgets/Windmill.lean
@@ -22,6 +22,7 @@ deriving DecidableEq, Repr, Inhabited,  Lean.ToJson, Lean.FromJson
 structure WindmillWidgetProps where
   triple? : Option WindmillTriple := none
   colors? : Option WindmillColors := some default
+  mirrow : Bool := false
   deriving Lean.Server.RpcEncodable
 
 open ProofWidgets
@@ -52,8 +53,12 @@ def WindmillWidget : Component WindmillWidgetProps where
         const squareSize = z * subSquareSize;
         const rectWidth = y * subSquareSize;
         const rectHeight = x * subSquareSize;
-        const startX = 120;
-        const startY = 120;
+
+        // Calculate the start positions to center the square in the view
+        const centerX = 200;  // Assuming the viewBox width is 400
+        const centerY = 200;  // Assuming the viewBox height is 400
+        const startX = centerX - (squareSize / 2);
+        const startY = centerY - (squareSize / 2);
 
         // Create SVG for the central square and the four rectangles
         const createSquares = () => {
@@ -118,6 +123,7 @@ def WindmillWidget : Component WindmillWidgetProps where
       }, React.createElement(WindmillPattern));
     }"
 
+
 def greyColors := ( some <| {
     square? := some "lightgrey",
     north? := some "lightgrey",

From 0f1e2f7001e0f585264d03080866b9a2c24ec583 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 20 Oct 2024 13:51:06 +0200
Subject: [PATCH 5/6] add mirror

---
 FormalBook/Chapter_04.lean       |  4 ++--
 FormalBook/Widgets/Windmill.lean | 21 +++++++++++++++------
 2 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/FormalBook/Chapter_04.lean b/FormalBook/Chapter_04.lean
index ffb85d8..c90ed3d 100644
--- a/FormalBook/Chapter_04.lean
+++ b/FormalBook/Chapter_04.lean
@@ -270,11 +270,11 @@ def xyz := ((4, 3, 5) : ℤ × ℤ × ℤ)
 def toTriple := fun (xyz : ℤ × ℤ × ℤ) ↦
     (some <|  {x := xyz.1.natAbs, y := xyz.2.1.natAbs, z := xyz.2.2.natAbs} : Option WindmillTriple)
 
-#widget WindmillWidget with { triple? :=(toTriple xyz) : WindmillWidgetProps }
+#widget WindmillWidget with ({ triple? :=toTriple xyz, mirror := true} : WindmillWidgetProps )
 
 -- ... and its winged shape
 
-#widget WindmillWidget with ({ triple? := (toTriple xyz), colors? := greyColors} : WindmillWidgetProps)
+#widget WindmillWidget with ({ triple? := (toTriple xyz), colors? := greyColors, mirror := true} : WindmillWidgetProps)
 
 -- The second winged derived from the windeg shape of are 73 using `secondInvo`:
 
diff --git a/FormalBook/Widgets/Windmill.lean b/FormalBook/Widgets/Windmill.lean
index 1b3fe6d..6daf189 100644
--- a/FormalBook/Widgets/Windmill.lean
+++ b/FormalBook/Widgets/Windmill.lean
@@ -22,7 +22,7 @@ deriving DecidableEq, Repr, Inhabited,  Lean.ToJson, Lean.FromJson
 structure WindmillWidgetProps where
   triple? : Option WindmillTriple := none
   colors? : Option WindmillColors := some default
-  mirrow : Bool := false
+  mirror : Bool := false
   deriving Lean.Server.RpcEncodable
 
 open ProofWidgets
@@ -38,9 +38,9 @@ def WindmillWidget : Component WindmillWidgetProps where
         const subSquareSize = 20;
 
         // Extract the values from props
-        const z = props.triple.z || 5;
-        const x = props.triple.x || 2;
-        const y = props.triple.y || 3;
+        const z = (props.triple && props.triple.z) || 5;
+        const x = (props.triple && props.triple.x) || 2;
+        const y = (props.triple && props.triple.y) || 3;
 
         // Use colors from props
         const colors = props.colors || {};
@@ -104,12 +104,17 @@ def WindmillWidget : Component WindmillWidgetProps where
           return elements;
         };
 
+        // Apply mirror transformation if mirror prop is true
+        const transformGroup = props.mirror
+          ? React.createElement('g', { transform: 'scale(-1,1) translate(-400,0)' }, createSquares())
+          : createSquares();
+
         return React.createElement('svg', {
           width: '100%',
           height: '100%',
           viewBox: '0 0 400 400',  // Adjust based on your SVG dimensions
           style: { display: 'block', margin: '0 auto' } // Center horizontally
-        }, createSquares());
+        }, transformGroup);
       };
 
       return React.createElement('div', {
@@ -123,7 +128,6 @@ def WindmillWidget : Component WindmillWidgetProps where
       }, React.createElement(WindmillPattern));
     }"
 
-
 def greyColors := ( some <| {
     square? := some "lightgrey",
     north? := some "lightgrey",
@@ -134,6 +138,11 @@ def greyColors := ( some <| {
 
 #widget WindmillWidget with { triple? := some <| {x := 2, y :=7, z := 3} : WindmillWidgetProps }
 
+#widget WindmillWidget with ({
+  triple? := some ({x := 2, y :=7, z := 3}),
+  mirror := True
+  }: WindmillWidgetProps)
+
 #widget WindmillWidget with { triple? := some <| {x := 5, y := 5, z := 3} : WindmillWidgetProps }
 
 #widget WindmillWidget with { triple? := some <| {x := 3, y := 7, z := 2} : WindmillWidgetProps }

From dbacf984f08c7a67fe189fcc6395925fa83d7556 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 20 Oct 2024 20:47:57 +0200
Subject: [PATCH 6/6] simplify

---
 FormalBook/Chapter_04.lean       | 8 +++++---
 FormalBook/Widgets/Windmill.lean | 2 +-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/FormalBook/Chapter_04.lean b/FormalBook/Chapter_04.lean
index c90ed3d..e5f1b16 100644
--- a/FormalBook/Chapter_04.lean
+++ b/FormalBook/Chapter_04.lean
@@ -263,18 +263,20 @@ theorem theorem₂ {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) :
 
 
 
--- The windged sqaure of area 4xy + z^2 = 73 that corresponds to (x,y,z) = (3,4,5)
+-- The windged square of area 4xy + z^2 = 73 that corresponds to (x,y,z) = (3,4,5)
 
 def xyz := ((4, 3, 5) : ℤ × ℤ × ℤ)
 
 def toTriple := fun (xyz : ℤ × ℤ × ℤ) ↦
     (some <|  {x := xyz.1.natAbs, y := xyz.2.1.natAbs, z := xyz.2.2.natAbs} : Option WindmillTriple)
 
-#widget WindmillWidget with ({ triple? :=toTriple xyz, mirror := true} : WindmillWidgetProps )
+#widget WindmillWidget with ({ triple? :=toTriple xyz, mirror := true} : WindmillWidgetProps)
 
 -- ... and its winged shape
 
-#widget WindmillWidget with ({ triple? := (toTriple xyz), colors? := greyColors, mirror := true} : WindmillWidgetProps)
+#widget WindmillWidget with ({ triple? := (toTriple xyz),
+                               colors? := greyColors,
+                               mirror := true} : WindmillWidgetProps)
 
 -- The second winged derived from the windeg shape of are 73 using `secondInvo`:
 
diff --git a/FormalBook/Widgets/Windmill.lean b/FormalBook/Widgets/Windmill.lean
index 6daf189..a80304d 100644
--- a/FormalBook/Widgets/Windmill.lean
+++ b/FormalBook/Widgets/Windmill.lean
@@ -112,7 +112,7 @@ def WindmillWidget : Component WindmillWidgetProps where
         return React.createElement('svg', {
           width: '100%',
           height: '100%',
-          viewBox: '0 0 400 400',  // Adjust based on your SVG dimensions
+          viewBox: '0 0 400 400',
           style: { display: 'block', margin: '0 auto' } // Center horizontally
         }, transformGroup);
       };