Three Erdős Problems and the Boundary of Witnessed Closure

This paper collects three elementary results from a formalized corpus of Erdős problems: the subset-sum injection bound, the complement-pairing bound for two-intersecting families, and a non-vacuity construction for the Erdős–Faber–Lovász hypothesis. Each result has an explicit witness and a complete checked proof. The results are deliberately separated from the stronger open or deep theorems that motivate them. The sharp distinct-subset-sum problem, the Frankl–Füredi extremal problem, and the full Erdős–Faber–Lovász theorem require methods not used here. The purpose of the paper is to state precisely what the elementary arguments prove and where they stop.