From 6b6875b31c24541dae97fe6bc960baf8fa3b2364 Mon Sep 17 00:00:00 2001 From: Cayden Codel Date: Sun, 9 Jun 2024 22:38:38 -0700 Subject: [PATCH] Rewrite ending paragraph of symm breaking section --- ITP/symmetry-breaking.tex | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/ITP/symmetry-breaking.tex b/ITP/symmetry-breaking.tex index 0f2dd16..e3d634d 100644 --- a/ITP/symmetry-breaking.tex +++ b/ITP/symmetry-breaking.tex @@ -131,14 +131,9 @@ 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. +Compared to the symmetry-breaking transformation described by Heule and Scheucher, +our transformation is simpler. +Nonetheless, proving the above theorem in Lean was tedious, +as we had to show that the properties from the previous steps were preserved at each new step, +which carried substantial proof burden. +In particular, steps 3 through 6 required careful bookkeeping and special handling of the distinguished point~$p_1$.