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

Proof of `Per-Client Fairness Parameters at Treewidth Four` (5th statement)

groundedproofs/Lax117284Proofs/Machine/MisFinal.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 number of colours, the number of vertices per colour, and the bits of the adjacency matrix; a first pass over the matrix checks that it is symmetric, has no loop and no edge inside a colour class; a second checks that the graph is regular of a positive degree and has an even number of edges, by counting the neighbours of every vertex; and the numbers of the image are then written cell by cell, the processing time and the due date of each job being a closed form computed from its day and its client: a case analysis on the kind of day — a vertex day, a validation day or the day of an edge, whose endpoints are found by scanning the matrix for the corresponding edge — and on the kind of client. The number of colours and the number of vertices are numbers of the input and are bounded by its length, since the image is only written for a graph. A word that is not the code of such a graph 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.