doc: record the n = 8 ISCAS85 results

10 of 11 circuits prove equivalent at n = 8, against 1 of 11 unpartitioned.
Both baseline failure modes are gone: nothing exhausts its unique table and
no conversion times out. Peak table occupancy across the whole suite stays
under 4506 entries where six circuits previously blew a 300000-entry table.

Records the partition shape per circuit alongside the verdicts, and notes
two results that need reading carefully:

c6288 still fails, but at a different stage. The converter handles it -
236 blocks, 5181 nodes - and it is the equivalence proof that exhausts the
ten minute budget on a 56373-variable miter. Expected for a 16x16 multiplier
and consistent with the known risk recorded earlier, but "cannot verify"
is a different problem from "cannot build".

c1355 comes out smaller than golden (888 -> 436) while everything else grows
1.4-1.8x. This is not a partitioning effect: c1355 is c499 with its XOR
trees expanded, so the two are the same function, and after resynthesis they
converge to 436 and 455 gates. The pass re-derives the function from its
diagrams and normalises the padded encoding away. The growth elsewhere is
the real cost of hard cut points at block boundaries.

Also ignores trace.vcd, the counterexample yosys dumps from a failed SAT
check, and updates the environment notes for the synth.sh fixes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014JTKS4uaDDZejKn7pE8vjc