Proof Complexity Notes

The paper I’ve been focusing on is Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs The idea is to figure out why the expander loss needs to be $o(1)$ instead of $O(1)$?

[Update 2026-09-06] My initial goal was to try and improve the result. I have not been able to do this yet. I read some of the background, and as I often forget, below are some notes for future self to references.