magma-1518-obstruction-lean: a Palomar-ready package, and two credit corrections

magma-1518-obstruction-lean grew a Palomar-ready package: Challenge.lean states Theorem A and the F_5 / F_13 members of Theorem F as coefficient matrices without imports, Solution.lean proves them from the core development and kernel decide, and a comparator pinned to Lean v4.33.0 accepts the pair locally — formalization.yaml, comparator.json and a PALOMAR.md readiness record are generated by scripts/gen_palomar.py.

Two README corrections followed. The minimality of 15 and the enumeration of the six non-isomorphic countermodels are Jose Brox’s, not a joint credit with Le Floch. And Tao’s Zulip message carries no finiteness hypothesis, so the improvement over it here is 3862 alone rather than four targets, with 3862 ⇒ 47/614/817 credited to Matthew Bolan’s Prover9 observation of November 2024 — eleven months before the finite-case observation the write-up already credits.