Verification of the union-closed-family bounds

../

union_closed/: A distinct PASS grade covers eight precise F and F_k conclusions; lower bounds have no unread theorem premise, while upper bounds retain Sauer–Shelah as an explicit external premise.

---

The whole-proof record separates the complete lower argument from the upper argument that consumes the supplied finite Sauer–Shelah theorem.