Machine-Checked Cost Model for a Karp Reduction: Independent Set to Clique in Lean 4

ABSTRACT This record contains a Lean 4 formalization of the classical Karp reductionfrom Independent Set to Clique via the graph complement, together with a costfunction defined independently of that construction and a machine-checkedtheorem linking the two. The point of the record is not the reduction, whichis textbook, but the form in which its resource cost is stated: the cost is aseparate structural recursion, the equality relating it to the construction isa theorem accepted by the kernel rather than a comment, and the degenerate wayof satisfying such an equality — defining one side through the other so thatit holds definitionally — is excluded by an explicit check rather than byconvention. The meaning of the two problems is pinned by universallyquantified specification theorems, so a definition fitted to a finite set oftested cases cannot satisfy them. No lower bound is established, and thechosen cost measure is not shown to be the correct model of a real executor'swork; both limits are stated in the accompanying write-up. FULL DESCRIPTION The folder is self-contained. It carries four Lean source files, a lakefile,a toolchain pin (leanprover/lean4:v4.19.0), a write-up, and a manifest. Stage 1 (LeanFormal/Basic.lean, 1566 bytes, SHA-256f5449a5168e32f103227ef6f3e2fb2a170f3101aef7198ee5dc8b758a59e715b, 5 theorems)formalizes a finite list transformation: reduce duplicates every bit, anyOnedetects a set bit, twoInRow detects two adjacent set bits. The theoremreduce_correct_and_cost proves, for every input word, both the correspondenceanyOne x = twoInRow (reduce x) and the exact cost steps x = 2 * length x. Themeasure steps is given by its own recursion on the input and does not mentionreduce; steps_eq relates the two separately. reduce_not_id witnesses that thereduction is not the identity. Stage 2 (LeanFormal/Karp.lean, 4366 bytes, SHA-256d84442baf5d79387b4e498094a9796c1cb922ae904c138e6bbfa559dc528178d, 13 theorems)formalizes the Independent Set / Clique pair. Four specification theorems —indep_spec, clique_spec, complement_spec, complement_verts — fix the meaningof the predicates and of the complement on all inputs, not on selectedexamples. reduce_correct_and_cost proves the universal equivalenceIsIndep g s <-> IsClique (complement g) s together with the exact coststeps g = |V| * |V|, where steps counts how many vertex pairs would have to beenumerated without building them; the link to the enumeration is a separateproved theorem. Reproduction is mechanical. The manifest records 11 claims; each is anidentifier, a value, and a command that runs from the folder and names a filein it. Every number appearing in the write-up carries such an identifier, so areader reproduces the figures instead of trusting them. Four artifacts arebyte-identical copies of their sources and are recorded with their SHA-256. Limits, stated deliberately. No lower bound follows: a reduction exhibits onealgorithm, not a statement about all of them. The cost measure is not shown tobe the correct model of real work — it counts pair enumeration and not themembership test performed inside the construction, so it is a lower measurethan the true cost of building the complement. Correspondence between theformal definitions and the notions as used in the literature is established byreading, not by execution. None of these gaps is closed by adding files.