Bipartite graphs on at most 25 vertices are 4-choosable

../

_proof: All possible palette sizes for a bad four-list assignment on at most 25 vertices are excluded by exact counting.

evidence/: Exact frozen subjects and independently graded mathematical scrutiny of the palette and incidence argument.

---

The proof reconstructs the palette-covering argument and specializes it to four-element lists. This argument by Plasma AI has the independently graded tier-1 warrant below, with no Lean proof or novelty claim. It uses no other native claim and does not rely on the numerical value of the four-uniform Property-B extremum or on the unproved Erdős–Rubin–Taylor footnote.

This supplies a lower bound for Problem 629, not the value of $n(4)$ or the answer for all $k$. The palette frontier records necessary conditions on a hypothetical bad assignment at order 26. Its evidence checks the displayed finite arithmetic, not existence or nonexistence of such an assignment. Verification of the claim consists of the merging argument, the covering inequality and the exact table in the proof. No mathematical gap remains in that stated lower bound.

Current standing and verification

Tier 1 records the independent whole-claim examination and its separate passing grade, both dated 2026-10-14. The reviewer and distinct grader each worked in a fresh, isolated context and disclosed GPT-6 Astra. The accepted verdict is refutation-failed for every finite simple bipartite graph through order 25, the complete palette argument and its exact arithmetic, and the consequence $n(4)\ge26$. The statement and complete mathematical proof match the frozen subject.

The report supplies an explicitly disclosed elementary construction on $K_{4,256}$ to check the nonemptiness required by the least-order notation. The grader accepts this as permitted well-definedness reconstruction, without attributing it to the frozen proof. Its examination of the arithmetic checker is documentary only; no execution or failure-exit coverage of that program is part of the grade. The complete arithmetic is retained in the report and grade, independently of the program.

The grade records qualified historical isolation evidence, not a certification of a complete interaction history. No native L-claim or external theorem is a proof premise; the cited method's specializations are proved in full. Bibliographic fidelity and novelty were not examined. The independently graded L78 gives the stronger bound $n(4)\ge27$; L25 retains its own accepted scope without determining the exact minimum or settling Problem 629.