Edge clique covers at packing defect one

A clique-edge packing is a set of edges of which no two belong to a common clique. We prove that every graph on n≥1 vertices with independence number at most two and maximum packing size n−1 has an edge clique cover of size n−1, extending the known equality for full packings. Given a legal packing of size n−1, the proof constructs either an (n−1)-clique cover or a packing of size n that deletes at most one original packed edge, together with an n-clique cover. The construction uses common neighborhoods of packed edges and resolves the exceptional path terminals by augmentation. Under the stated adjacency-matrix and packing-list promises, it takes O(n²) word operations, including the output lists. This record contains an unreviewed research preprint and its reproducibility materials: a 25-page manuscript, the matching LaTeX source archive, and Supplementary Material S1. S1 contains the Lean 4.33.0 development, pinned dependency files, the executable constructor, independent certificate checkers, and verification records. Its README provides reproduction commands. The formal development establishes the original finite-graph theorems and the promised-input constructor and its resource bounds. The additional eleven-vertex comparison example has a hand proof and an independent finite checker. Executable tests and internal reviews are supporting evidence, not external peer review or a certification of novelty. AI assistance: OpenAI tools assisted with proof discovery and development, argument reconstruction, literature comparison, verification code and Lean proofs, internal AI review, exposition, bibliography, and typesetting. The human author assumes responsibility for all mathematical statements and citations. Funding: This research received no external funding. Conflicts of interest: The author declares no conflicts of interest. Licenses: CC BY 4.0 applies to the manuscript and prose research documentation; MIT applies to the author-controlled code, build configuration, tests and certificates. See LICENSES.txt for the precise scope and third-party exclusions.