docs(tables): correct the stale per-table census and name its derivation

[MauroToscano]

The per-table census above max_rows in prover/src/tables/mod.rs was stale in
three rows and wrong in its formula. It has misled width and VRAM arithmetic more
than once, each time caught only because someone re-derived the numbers from
source instead of trusting the table. This corrects it and writes down how to
re-derive it, so the next drift is visible rather than silent.

Documentation only: the fourteen max_rows constants are byte-for-byte unchanged.

⚠ The diff does touch those fourteen lines, and it should not be read as a value change. Each
carries a trailing // … eff. width N comment, and it is the comment that moves — the widths there
were the inflated ones. Every 1 << N is identical before and after; the constants were extracted
and compared programmatically rather than eyeballed. Nothing in this change alters chunk geometry.

What was wrong, and by how much

Table	was	is
CPU	74 main, 40 bus	38 main, 20 bus
MUL	16 bus	24 bus
SHIFT	27 main, 15 bus	29 main, 18 bus
LT	15 main	17 main

CPU was the worst of these: nearly double its real main width and double its real
bus count, which compounds into a ~2.9× overstatement of its effective width.

Every row in the new table was executed, not read. auto_storage already
imports each table's bus_interactions and cols::NUM_COLUMNS, so a throwaway
in-crate test can call all fourteen and print the counts; that probe produced the
numbers below and was then reverted, leaving only the doc change. Counting
.push() calls by brace-matching is what produced the stale table in the first
place — several of these bodies build their vectors through loops over column
arrays, where a static count is exactly the thing that goes wrong.

The formula itself double-counted the bus term

The header read Effective width = main_cols + 3 × bus_interactions. That is
wrong, and it is the more consequential defect, because it is the part that
survives any refresh of the numbers.

LogUp does not commit one extension column per bus interaction. It commits
⌈Bus/2⌉ of them: crypto/stark/src/lookup.rs:939-944 sets
num_aux_columns = num_term_columns + 1 for a non-empty interaction set, and
num_term_columns is split_interactions' committed-pair count — 0 for
N ≤ 2, (N−1)/2 for odd N, (N−2)/2 for even N. All four branches work
out to exactly ⌈N/2⌉ for every N ≥ 1. So the effective width is

Eff.width = Main + 3 × ⌈Bus/2⌉

auto_storage::aux_cols states that same closed form directly as
bus_count.div_ceil(2), which is a useful corroboration — but that module sits
behind #[cfg(feature = "disk-spill")], so stark::lookup is the
always-compiled source of truth and the doc now points there.

Why this correction is right rather than merely different

The header also states the sizing rule: scale each table against MEMW's chunk
geometry. That rule is now checkable, and it comes out cleanly at the corrected
widths and badly at the old ones.

At the corrected widths, nearest 2^N of (88 × 2^19) / Eff.width reproduces
eight tables exactly — MEMW, CPU, CPU32, DVRM, MUL, SHIFT, BYTEWISE, LT.
Five more (LOAD, BRANCH, MEMW_R, EQ, STORE) land above 2^20 and ship at 2^20,
which is the ceiling every table in the module respects. MEMW_A keeps its
existing footnote: the ratio gives 2^20 and it is deliberately set to 2^19 to
match MEMW chunk geometry. That accounts for all fourteen.

Under the old widths the same rule put CPU at 2^18 against a shipped 2^19,
and no cap explains a table sized below the baseline. The old table was not
merely out of date — it was internally inconsistent with the rule printed
directly above it.

Scope

Pure documentation, stated as a verified negative rather than left implicit:
effective_width and Eff.width occur in exactly two places in the workspace,
both inside this doc comment. Nothing computes or consumes the Main / Bus /
Eff.width columns, so there is no behaviour to test and no constant to re-pin.

The table also gains the four auxiliary chips that were already in max_rows but
missing from it — CPU32, BYTEWISE, STORE, EQ — so its rows now match the module's
constants one-to-one.

Deliberately not in this change

The shipped max_rows values were scaled through the inflated bus term, which
penalises tables with a high bus-to-main ratio roughly twice as hard as it should
— DVRM, at 34 bus interactions against 34 main columns, is the extreme case.
At the corrected widths those tables land in a defensible place (DVRM 85 and CPU
68 against MEMW's 88), but the ratios that justified the constants were not the
ratios the code actually has.

Re-tuning the constants changes chunk geometry and therefore prover parallelism
and peak memory. That is a measured change, not a documentation one, and it is
left for a pass that can run the benchmark. This PR changes no constant.

Corroboration

Three independent routes produced this census and agree on every cell: executing
bus_interactions() directly, reading and brace-matching the function bodies,
and inverting the prover's run-time walk weights to recover CPU's main and aux
widths. A table three methods agree on is a different object from one person's
re-read, which is what the previous table was.