From bebf7a3fe263abce2fd9b0fba0f18f1a57da6dee Mon Sep 17 00:00:00 2001 From: James Date: Sun, 9 Jun 2024 00:33:13 -0400 Subject: [PATCH] remove symmetry breaking discussion (moving to a separate PR) --- ITP/symmetry-breaking.tex | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/ITP/symmetry-breaking.tex b/ITP/symmetry-breaking.tex index 0f2dd16..3f4e757 100644 --- a/ITP/symmetry-breaking.tex +++ b/ITP/symmetry-breaking.tex @@ -130,15 +130,3 @@ \end{align*} This concludes the proof. \end{proof} - -We had quite some difficulty formalizing the symmetry-breaking argument. -We spent many hours around a whiteboard, -simplifying the argument to minimize the amount of theory we would need to develop. -The projective transformation in Step 3 was particularly difficult to wrangle. -This step, and those after it, requires careful bookkeeping around the distinguished point $p_1$. - -Once these details were worked out, -the proof was relatively straightforward, albeit long and tedious. -Each step of the proof justifies not only that a new property is achieved, -but also that all properties from previous steps are preserved. -As a result, the proof burden was substantial.