More angle bisection lemmas #30474, #30476, #30477, ...

Stream: PR reviews

[Joseph Myers]

I currently have eight PRs open in the series working towards the relation of angle bisection to incenter and excenter: #30474, #30476, #30477, #30485, #30521, #30522, #30598, #30600.

[Joseph Myers]

I've just opened five more PRs in this series: #30698, #30699, #30700, #30702, #30703, so currently 13 open PRs in the series (I also have some not-yet-PRed material depending on most of the PRs in the series to strengthen the results of #30477 and go from there to statements involving angles between three points rather than angles with orthogonal projections).

[Joseph Myers]

Current open PRs in this series where comments have been addressed, needing review again: #30698, #30702. Current open PRs in this series needing review, no comments so far and no dependencies: #30485, #30522, #30598. Current open PRs in this series needing review, no comments so far, but depend on other PRs in the series: #30474, #30477, #30600, #30703.

[Joseph Myers]

Also now #30916 and #30918 (no dependencies).

[Joseph Myers]

And also #30935 (no dependencies), #30938 (depends on #30916). I now have all the material ready for the final two PRs on this series that actually relate incenter/excenter to angle bisection, to be opened once more of the dependencies are in. (It turns out #30485 (touchpoints are not vertices) is not needed for those final PRs after all, but I think it still makes sense as API lemmas.)

[Joseph Myers]

Thanks for the reviews! #30474, #30600, #30703 and #30938 are now unblocked (no further dependencies); #30477 depends on #30474. I've also opened the last two PRs in this series, #30981 and #30982, which show where it is heading. (#30943 isn't part of this series but the next one, lemmas that come up while formalizing IMO 2024 P4; I don't know how long that series will end up being since that formalization is in its early stages.)

[Joseph Myers]

Thanks for the further reviews! The remaining PRs in this series are the larger ones: #30477 is now unblocked, then #30981 depends on #30477 and #30982 depends on #30981.

[Joseph Myers]

I'd like to ping #30477 as the next PR in this series, all of whose dependencies are now merged.

[Joseph Myers]

I'd like to ping #30477 again (submitted a month ago, no review comments, has two further PRs depending on it that also have no review comments).

[Joseph Myers]

I'd like to ping the remaining two PRs in this series again: #30981 and #30982, both open since October with no review comments at all. (You could see #32282 - relating incenter/excenter to unoriented angle bisection - as an extension of the series, but that one has a lot of dependencies at present.)

[Joseph Myers]

I'd like to ping #30981 and #30982 (no reviews so far) again.