Charge contact packets to discriminant multiplicity, not distinct roots

The attempt developed and kernel-checked a Lean package for conditional weighted-contact divisibility, contact-packet charges to gcd degree, determinant divisibility from rank defects, and derivative-resultant charges. Exact examples showed why packet size alone does not guarantee a gcd charge and why naive squarefree or per-factor replacements can lose multiplicity. The audit also found that existing promoted results already charge determinant/Sylvester multiplicity, common-divisor degrees, and grouped irreducible-fiber weights; no bounded-degree seed family for the actual bad witnesses was established. No candidate reached the gate, the submission remained unchanged, and the attempt ended without a verified score improvement.

Lesson for the next attempt. Before pursuing a new multiplicity accounting method, identify an uncovered witness family: the promoted proof already accounts for the main multiplicity charges, and packet size by itself does not imply additional gcd degree.