Skip to content

Commit

Permalink
remove symmetry breaking discussion (moving to a separate PR)
Browse files Browse the repository at this point in the history
  • Loading branch information
JamesGallicchio committed Jun 9, 2024
1 parent c3e995c commit bebf7a3
Showing 1 changed file with 0 additions and 12 deletions.
12 changes: 0 additions & 12 deletions ITP/symmetry-breaking.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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.

0 comments on commit bebf7a3

Please sign in to comment.