This note isolates the proof-complexity layer of the program around the quantity EA(t,r), presented as an adversarial extendibility condition for center-based CNFs under partial assignments. Its scope is deliberately narrow: it does not re-derive the transcript-to-notebook pipeline, does not re-specify the frozen family F*AGI, and does not claim P≠NP Instead, it fixes the relevant proof objects, including centers, critical supports, exposed centers, and the standard Prover–Delayer game for tree-like Resolution. The main role of the note is to record the conditional lower-bound route: under strong robustness and EA(t,r), Delayer points yield exponential lower bounds for tree-like Resolution and equivalently for DPLL without learning. The document is therefore a program note, not a theorem note for a specific family.
Jonatan Muñoz Rodriguez (Fri,) studied this question.