Hanlin Ren of the Institute for Advanced Study continues his two-part seminar on why fundamental complexity lower bounds, like P versus NP, resist proof, arguing the obstacle may be logical rather than combinatorial. Rather than asking which lower bounds can be proved, Ren asks what axioms are strictly necessary to prove them, drawing on bounded arithmetic and feasible mathematics. He revisits Klaus Maass's 1984 result that one-tape Turing machines need quadratic time to recognize palindromes, showing it is logically equivalent to the weak pigeonhole principle over the base theory PV. He then turns to the Resolution proof system, where hardness proofs require a specific threshold of logical strength, T^1_2 plus dwPHP(PV), independent of which hard tautology is used. The talk draws on papers by Oliver Korten, by Lijie Chen, Jiatu Li, and Igor Oliveira, and Ren's own work with Jiawei Li and Yuhao Li. No background in bounded arithmetic is assumed, and the talk builds the framework from first principles across its two-hour session.