Verify Chvátal's conjecture on intersecting families in downsets for the 8-element ground set (Erdős #701)

A family $\mathcal{F}$ of finite sets is a *downset* (closed under taking subsets) if $B\subseteq A\in\mathcal{F}$ implies $B\in\mathcal{F}$. A subfamily $\mathcal{F}'\subseteq\mathcal{F}$ is *intersecting* if $A\cap B\neq\varnothing$ for all $A,B\in\mathcal{F}'$. For an element $x$, the *star* $\mathcal{S}_x=\{A\in\mathcal{F}:x\in A\}$ is always intersecting. Chvátal's conjecture asserts that for every downset $\mathcal{F}$ there is an element $x$ such that every intersecting subfamily satisfies $\lvert\mathcal{F}'\rvert\le\lvert\mathcal{S}_x\rvert$ — i.e. some star is a maximum intersecting subfamily. Concrete target: verify the conjecture for **all** downsets on a ground set of size $n=8$ (or find a counterexample on $\le 8$ elements).

Acceptance. FULLY RESOLVES (for $n=8$): a verification that for every downset on $\{1,\dots,8\}$ some star is a maximum intersecting subfamily — delivered as an exact/certified computation (e.g. rational IP certificates as in ChvatalIP, or exhaustive enumeration with a machine-checkable proof), OR an explicit counterexample downset on $\le 8$ elements with a verified larger-than-any-star intersecting subfamily. PARTIAL: a certified verification restricted to a structured subclass on $8$ elements (bounded rank/width), or an algorithm demonstrably scaling past the $n=7$ record.