While this submission is a draft, it cannot be used by other submissions.

Proof of `Three Days and the Fairness Parameter One` (5th statement)

groundedproofs/Lax117284Proofs/Machine/SatFinal.lean · lax-117284

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The reduction is a word RAM program on the zeros and ones of its input: a one-pass tokenizer reads the formula — the number of variables, the numbers of clauses of two and of three literals, and a variable and a sign for every position —, a first pass checks, for every position, that its variable is one of the formula's and that its literal has not occurred twice before it, which is a loop over the earlier positions that counts, and a second pass writes the image, the due date of every client on each of the three days being a case analysis on the number of the client that counts, on the third day, the earlier positions with the same literal. The number of variables is required not to exceed the number of positions, which keeps the image polynomial in the input. A word that is not the code of such a formula is answered with the rejected word. The numbers may be exponential in the length of the input, which the word length of a polynomial-time word RAM accommodates, and polynomial time on the word RAM transfers to a Turing machine.