The witness is the compiled driver $driverProgram (table q k)$, with $q = rank φ$ — the tree-fold schema of $TreeFold.lean$, instantiated with the type table of $MsoTable.lean$ and given the instance word's front end.

The mathematics is finished before the program is looked at. $val_eq_typeOf$ says the fold's value at a node is the number of the $q$-type of the subexpression rooted there, by structural induction on the expression with one congruence of $MsoCliqueOps.lean$ per constructor; $acceptVal_val$ turns the value at the root into the truth of the sentence, by adequacy and the root conditions of $ValidFor$. Both are statements about the pure fold, with no environment in them.

What is left is the word. $instance_tape$ decomposes an admissible input into the segments the reads consume — two header entries, the rest of the graph block, the node count, and three arrays of one entry per node — and $encExpr_of_encodesExpr$ forgets the surface encoding relation to the one the induction is stated against. $driverCom_run$ then runs the phases in a row: the graph block and the vertex-name array are read into arrays nothing ever reads again, the parents and the op codes into the schema's own, the four tables are materialized by $stores_arrOf_run$, and $seedLoop_run$ and $pushLoop_run$ do the fold. The epilogue is one $write$ of $acp[acc[N-1]]$, which is in range because the root's value is the number of a type.

$computesInTime_of_solves$ discharges the compiler, the layout invariant and the machine, charging $layout.const = 10$ machine steps per unit of IMP+ cost, plus one for the final $halt$. The array extents are chosen per input, as that lemma allows.

The bound is $10 * (100 + driverCost (table q k))$ per entry of the input word. The first factor is the compiler — an array access compiles to four instructions, whatever the layout — and the hundred is the driver's own per-entry cost, every loop bounded loosely and nothing fought over. The third term is the price of materializing the four tables, three units per entry, and it is where the tower lives: the type table has one row and one column per $q$-type of a $k$-labelled region, a number that grows faster than any tower of exponentials in $q$. It is paid once, before the input is read, which the order of the quantifiers permits — the sentence and the width bound come first, then the program and the constant, then the graph.

The input is nonempty and the table setup cost is positive. Spreading that one-time cost over the whole input leaves enough slack in the same constant to pay the final $halt$ instruction.

What the theorem claims about that constant is that it depends on the sentence and the width bound alone: the tables are materialized before the input is read, and the per-node work of the fold is a fixed number of array accesses whatever the size of the alphabet. What it does not claim is any bound on it. None is computed anywhere in the development, and the absence is deliberate rather than an oversight — every known proof of Courcelle's theorem makes the dependence non-elementary.

The machine truncates every value modulo $2 ^ w$, so the run on the machine is the run in the unbounded semantics only as long as nothing the program computes reaches $2 ^ w$. The bound the driver is proved under is $driverBound$: the length of the input word, plus its largest entry, plus the size of the tables. All three summands are needed and none of them is loose.

The length. Every count the program keeps — the number of nodes, the length of the graph block, the loop counters, the offsets into the four arrays of the expression block — is a count of entries of the word.

The largest entry. Most entries of an instance are small: vertex numbers, offsets and node numbers are below the length of the word, and an operation code is below the number of operations at width $k$, which the tables' size already covers. Two families are not, because the encoding deliberately does not constrain them — the parent entry of the root, which nothing points through, and the vertex name at a node whose operation creates no vertex. The machine reads its whole tape whatever it does with it, so those entries pass through the accumulator and have to be words; there is nothing to prove about them and nothing to be gained by pretending they are small, so the bound names the largest entry and the statement's fitting condition supplies it. That is the only reason the condition quantifies over the entries of the word rather than over its length alone.

The tables. A label indexes the array of seeds and a cell of the square combination table is indexed by two values at once, so $T.L$ and $T.V * T.V$ are numbers the machine holds. This is the one place where the size of the type alphabet — the tower — reaches the word length rather than only the constant, and it is honest that it does: a machine whose words cannot number the types cannot run the table. It costs the statement nothing, because the constant is chosen after the sentence and the width bound, and $tableSpan_le_driverCost$ says the constant that pays for materializing the table already pays for holding its indices.

So the compiled program needs $13 + 9 * driverBound$ cells to be words, and the statement's hypothesis — that $10 * (100 + driverCost) * (|x| + v + 1)$ is a word for every entry $v$ — gives that at the largest entry, with a margin nobody has to compute.

These are the honesty items of the theorem: what the statement claims, where it and a textbook proof part company, and what a reader is entitled to know was decided rather than proved. The definitions carry their own notes — the logic in $Lax11.Mso$, $k$-expressions in $Lax11.CliqueExpr$, the input format in $Lax11.InstanceEncoding$ — and what is said there is not repeated here.

The width measure is cliquewidth, and the conversion from treewidth is not formalized. What is proved is the Courcelle–Makowsky–Rotics form: MSO₁ model checking in linear time on graphs presented with a $k$-expression. Bounded treewidth implies bounded cliquewidth, so the class covered here contains every class of bounded treewidth; but getting the treewidth form of the statement out of this one needs a conversion of a tree decomposition of width $w$ into a $k$-expression with $k$ bounded in terms of $w$, and that conversion is not formalized. Anyone who wants the treewidth statement should treat it as unproved here. The same holds one level up, at the input: the theorem takes a $k$-expression, it does not compute one. Deciding cliquewidth is NP-hard and approximating it is the theorem of Oum and Seymour; neither is in this submission. That is exactly the status a linear-time treewidth algorithm would have had — a separate theorem, with its own proof, which composes with this one to give an algorithm that takes only the graph.

The expression is a certificate, and the program reads only two of its arrays. The program never looks at the compressed sparse row block, and never at the vertex-name array of the expression block: it reads the whole word, because it must get past the graph block to reach the expression block and because the machine reads its tape in order, but it uses only the parent array and the operation-code array. The other two go into arrays no later expression of the program mentions. This is not laziness dressed up: the type of a subexpression is a function of the types of its children and of the operation at its root, and of nothing else. The graph block is what makes $Sat G φ$ refer to a graph in the first place, and the vertex names are what make the second block a $k$-expression rather than the shape of one, so that a reviewer can check the certificate against the graph. Both only lengthen the input, so reading past them costs a constant per entry and the bound is unaffected.

The type table is noncomputable, and that is the shape of the statement. The fold is driven by a table — a finite value alphabet, an initial value per operation symbol, a binary combination. Here the values are the $q$-types of $k$-labelled regions, and the table is extracted from the composition congruences by $Fintype$ together with choice: for each pair of types the entry is a type realized by some gluing of two regions with those types, and the congruences say that the choice does not matter. Nothing in the development computes this table, and nothing could — the statement is an existential over programs, and the truth of a monadic second-order sentence in an arbitrary graph is not something the meta level decides on the way to constructing one. A reader who wants the machine to print the table is asking for an effective bound on the type space, which is the tower this development declines to estimate. What the noncomputability does not touch is the program: $table q k$ is a noncomputable inhabitant of an ordinary structure type and the generator consumes it as data, so the same generator applied to a computable table produces a program that runs. The table's content is carried by proof; the program text around it is carried by evaluation.

The multiplication instruction is never used. The machine of $Lax67.Ram$ has one, and under a unit-cost measure a linear-time claim that leans on it is at risk of being an artifact of the model. The fold indexes a two-dimensional table, which is where a multiplication would naturally appear — the entry for $a$ and $b$ sits at $a·V + b$. Instead the row bases $a·V$ are themselves materialized, once, in the prologue, as the array $row$, and a lookup is $tab[row[a] + b]$: two array reads and an addition. The prologue that fills $row$ is a sequence of stores whose length is the table's size, a constant fixed before the input is read. So the compiled program contains no multiplication anywhere — $CourcelleDriver.lean$ checks that by filtering the generated instruction list, since it is a property of the program text and the program text is the same for every table — and the claim survives the strictest reading of the cost model, the one that would charge for a product of two words, rather than depending on a generous one.

The machine-versus-model check runs a stand-in table. House discipline in this submission is that every program is run — by `#eval` inside the build, against the pure model it is proved to implement — before anything about it is proved. The driver is run that way, but it cannot be run with the type table, which is noncomputable by construction. $CourcelleDriver.lean$ therefore instantiates the generic driver with $edgeTable$: a hand-written table over the same operation alphabet, decoded by the same $Op.decode$, whose values are three bits — class $0$ is nonempty, class $1$ is nonempty, there is an edge — together with the partial states the sequential fold needs. That is a genuine cliquewidth dynamic program, and the two sentences it decides on the path $0—1—2$ are "some two vertices are adjacent" and its negation; the machine writes $1$ and $0$, and `#guard`s check that against the pure fold. So every line of program text is exercised: the same reads, the same prologue, the same seed and push loops, the same epilogue, the same decoder. What is not exercised is the content of the real table, and that is exactly what $val_eq_typeOf$ carries. Plumbing is machine-checked, mathematics is proof-carried, and neither is asked to vouch for the other.

$TreeDecomp.lean$ is imported by nothing in the proof. It is a self-contained file of tree-decomposition theory — descendants as parent-map iteration, validity and width, the tree order, the highest node containing a vertex, subtrees as unions of bags, the separation lemma and the edge-placement lemmas — stated in the numbering the encoding uses, and it is named here so that no reviewer spends time looking for the place where it is used.

One device on the trust surface is not textbook. Everything a reader has to check by eye — the machine, what it means to compute within a time bound, the graph encoding, the syntax and satisfaction of the logic, $k$-expressions and their evaluation, the input format, and the statement itself — is written to be the object a paper would write, with one exception, and it should be named plainly. Variables in formulas are de Bruijn positions, so a reader checking $Lax11.Mso$ against a textbook must translate between $∃x. ∃y. adj(x, y)$ and $MSO.exV (MSO.exV (MSO.adj 0 1))$, and must hold in mind that a quantifier binds at the last position, so that the outermost variable is $0$ and no index is ever shifted. Every other deviation in this development is inside the proof package, where the kernel is the reviewer. This one is not, and it is the price paid for keeping substitution off the surface entirely.

Courcelle's theorem in the Courcelle–Makowsky–Rotics form: monadic second-order model checking in linear time on graphs of bounded cliquewidth, given a $k$-expression. The type algebra and the composition lemma are the standard Ehrenfeucht–Fraïssé argument; the program is the textbook bottom-up fold.