An unnamed polynomial is not automatically an error

An existence theorem may legitimately assert $\exists P$ without displaying coefficients in its statement. A fully specified algorithm and a proof of a polynomial bound can establish that assertion.

The plan's demand is narrower and more concrete: the finite certificate should name the polynomial used in its ledger. Equation (eq:resource-polynomial) does so for the independently defined partial family. It is not advertised as the resource polynomial of the external general construction.

To certify an extracted source instance, one would need its actual generator, gate expansion, denominator bounds, controlled arithmetic circuits, and inverse-work ledger. Naming a large polynomial without establishing those inequalities would not fill that gap.