Acknowledgments

Thanks to Monica Omar on Lean Zulip, who closed the 6-level Finset.sum commutation in the Conv2D VJP proof.

Thanks to Franz Huschenbeth on Lean Zulip for reviewing early drafts and suggesting the comparator approach used in Appendix B.