# mod3-circuit-size: Knuth's open case C(S_{1,4}(x1,…,x6)) — is size(MOD3,1 on 6 inputs) = 13?

Status first, so nobody mistakes the small print: **this directory does not
approach P vs NP.** It attacks the smallest published open cell at the finite
base of the circuit-lower-bound programme — the exact minimum number of binary
gates for one explicit 6-input function — with SAT solving, DRAT proofs, and
Lean-checked certificates. A complete answer here is a theorem about one
function; it says nothing about asymptotic lower bounds.

**Public page:** https://mod3-circuit-size.pages.dev/ (results note, paper PDF, this README, and a
certificate archive with SHA-256; deployed on Cloudflare Pages 2026-08-23).

## Statement

A *Boolean chain* (circuit over the full binary basis B2) on inputs x1..xn is a
sequence of steps x_i = x_j ∘_i x_k (n < i ≤ n+s, 1 ≤ j < k < i), ∘_i any of the
16 binary operations. Its *cost* is s. C(f) = minimum cost of a chain with
some step equal to f (Knuth, TAOCP 7.1.2; C(f) = C(¬f), and every f is
computed by a *normal* chain — all ops map (0,0)↦0 — of cost C(f ⊕ f(0))).

    MOD3,r_n(x) = [x1 + … + xn ≡ r (mod 3)]          (Knuth writes S_{r, r+3, …})

**Knuth's conjecture** (TAOCP 7.2.2.2, answer to exercise 480): for n ≥ 3,
C(MOD3,r_n) = 3n − 5 − [(n+r) ≡ 0 mod 3]. Known: true for n ≤ 5 (Knuth, SAT)
and for (n,r) = (6,0) (Biere 2014 / Knuth); upper bound for all n, r
(Kulikov–Pechenev–Slezkin 2022, Thm 1). **The open cell:** n = 6, r ∈ {1,2}
(equivalent under x ↦ ¬x, which is free in B2): conjectured value 13, known
13 ≥ C ≥ ?. Knuth: "The case n = 6 and a ≠ 0, which lies tantalizingly close
to the limits of today's solvers, is still unknown. What is C(S_{1,4}(x1,…,x6))?"

*Complete answer:* C(MOD3,1_6) = 13, i.e. a 13-step chain (exists, below) and a
proof that no chain of cost ≤ 12 computes it. *Partial answer:* a proof for
cost ≤ s for some s < 12 (a lower bound), with the reach honestly measured.

## Prior status

| Scope | Status | Source |
|---|---|---|
| C(MOD3,r_n) for n=3,4,5: (3,4,4), (7,7,6), (10,9,10) | proved (SAT, not ours) | Knuth, TAOCP Vol 4 Fasc 6 (2015) / Vol 4B, answer 480(c) |
| C(MOD3,0_6) = 12 | proved (SAT; chain found by A. Biere 2014; not ours) | ibid. |
| C(MOD3,r_n) ≤ 3n−5−[(n+r)≡0 mod 3], all n ≥ 3 | proved (explicit blocks; not ours) | Kulikov, Pechenev, Slezkin, MFCS 2022 / arXiv:2102.12579, Thm 1 |
| n=6, r≠0 | **open** | Knuth, answer 480: "still unknown"; KPS §1: "To prove Knuth's conjecture, one also needs to prove a lower bound" |
| general lower bound for MOD3 | 2.5n − O(1) (Stockmeyer 1977) | quoted in KPS |
| Vol 4B errata through 2026-04-17 | only a typo fix in answer 480(c) (ν_{n−3} → ν_{n+3}, 2025-01-02); no change to "still unknown" | err4b.ps.gz, Knuth's site |

Literature check performed 2026-08-22 (web search + the 2025 "Simplifier" paper
from the same group + Feb-2026 gate-elimination preprint): no resolution found.

## Ground-truth anchors

| Quantity | Published value | Source | Reproduced? |
|---|---|---|---|
| Full adder (maj, xor on 3 inputs): cost 5 | 5 | Knuth 7.1.2 | ✓ UNSAT at 4 (DRAT), SAT at 5 (verified) |
| Knuth's encoding size for the full adder, answer 478: (N4,N5)=(82,115) vars, (M4,M5)=(942,1662) clauses | 82/942, 115/1662 | Knuth, answer 478 | ✓ exactly (encoder A with the answer-477 optional clauses, no colex) |
| C(MOD3,r_n), n=3: 3,4,4; n=4: 7,7,6; n=5: 10,9,10 | Knuth, answer 480 | ✓ all nine values: n=3,4 by encoder A, encoder B, and exhaustive enumeration; n=5 by encoder A (plain, DRAT: (5,0,9) 13 989 s, (5,2,9) 4460 s, (5,1,8) 66 s) and encoder B (plain, DRAT: 3403 s, 2372 s, 60 s) |
| Number of normal 4-variable functions of cost ≤ s: 5, 35, 263, 1500, 6812, 18904, 31408 (s=0..6) | Knuth 7.1.2 Table 1 (halved: C(f)=C(¬f)) | ✓ exhaustive enumerator `enum_chains.c` (no SAT) |
| Biere's 12-step chain for ¬MOD3,0_6 | Knuth, answer 480 | ✓ transcribed, verified in Python and Lean kernel |
| C(MOD3,0_6) = 12 (UNSAT at 11) | Knuth | **not reproduced** (both runs still going after 12 h; not used in R7); SAT half ✓ (Biere's chain, Lean; our own `fo_6_0_s12`) |
| The unique 5-variable class with C(f)=12 (truth table 169ae443) | Knuth 7.1.2 | not finished (killed to free cores; not used) |

## Results

(Being filled in as runs complete; every row is backed by a file in `results/`.)

| # | Claim | Status | How to check |
|---|---|---|---|
| R1 | C(MOD3,1_6) ≤ 13: explicit 13-step chain (IN2+MID3+OUT_1^1 of KPS) | **machine-verified** (Lean kernel `decide`, 64 inputs, with negative control); construction not ours | `python3 code/verify_chain.py results/kps-mod3-1-6.chain`; `lean lean/KPSMod3_1_6.lean` |
| R2 | Biere's 12-step chain computes ¬MOD3,0_6 | machine-verified (Lean kernel) | `lean lean/BiereMod3_0_6.lean` |
| R3 | anchors n=3,4 (9 cells, SAT and UNSAT halves) | machine-verified: SAT certificates verified by `verify_chain.py`; UNSAT by drat-trim; two encodings (A,B) agree; n=4 also by exhaustive enumeration | `results/anchors-A.tsv`, `results/anchors-B.tsv`, `code/enum_chains 4 6` |
| R4 | C(MOD3,1_6) ≥ 11 — no chain of cost ≤ 10 | **proved** by Lemma 2 from C(MOD3,0_5)=10 (Knuth; DRAT re-proof here in `fo_5_0_s9`); (6,1,9) also UNSAT by plain SAT (576 s, DRAT) | `results/target-small.tsv`, `results/fanout-anchors.tsv` |
| R5 | No chain of cost 11 for MOD3,1_6 (so C ≥ 12) | **machine-verified**: UNSAT with Lemma-2 clauses (fanout ≤ 1), cadical 166 s, DRAT checked 239 s | `results/fanout-anchors.tsv` row `fo_6_1_s11`; re-run: `python3 code/encode_a.py 6 11 mod3:1 --symin --lastout --fanout-max 1 --out x.cnf && python3 code/solve.py x.cnf --solver cadical --proof x.drat --check-proof` |
| R6 | Our own 13-step chain for MOD3,1_6 (found by SAT, independent of KPS) | machine-verified (Lean kernel) | `lean lean/SatMod3_1_6_s13.lean` |
| R7 | **No chain of cost 12, hence C(MOD3,1_6) = C(MOD3,2_6) = 13** (Knuth's conjecture at n = 6, r ≠ 0) | **machine-verified** (cube-and-conquer; every cube's DRAT proof checked by drat-trim; cube cover proved by a DRAT-checked refutation — see "The s = 12 run") | `results/cnf/gp_6_1_s12_d4.cubes.tsv`, `..._d5a/_d5b.cubes.tsv`, `results/cnf/gp_6_1_s12.cnf.cover.ok`; `bash code/verify_all.sh` |
| R9 | C(MOD3,0_6) = 12 (Knuth's value, now reproduced in-house) | **machine-verified**: UNSAT at 11 with Lemmas 1–3 (fanout ≤ 1, gelim 10:10), cadical 0.1 s, DRAT; SAT half = Biere's chain (Lean) | `results/logs/ge_6_0_s11.log`, `lean/BiereMod3_0_6.lean` |
| R10 | **C(MOD3,2_7) = 15** — a new cell of Knuth's conjecture (n = 7, r = 2: 3·7−5−1 = 15) | **machine-verified**: UNSAT at 14 with Lemmas 1–3 (fanout ≤ 1 from C(MOD3,1_6) = C(MOD3,2_6) = 13, R7), cadical 0.4 s, DRAT; 15-step chain (KPS blocks IN4+OUT_3^2) verified in Lean | `results/logs/ge_7_2_s14.log`, `results/kps-mod3-2-7.chain`, `lean/KPSMod3_2_7.lean` |
| R11 | C(MOD3,0_7) ≥ 15, C(MOD3,1_7) ≥ 15 (conjectured 16; KPS chains of 16 verified in Lean) | **machine-verified** lower bounds: UNSAT at 14 (gelim 12:13 resp. 13:12; fanout ≤ 1), DRAT, 1.2 s / 7.2 s | `results/logs/ge_7_0_s14.log`, `ge_7_1_s14.log`; `lean/KPSMod3_0_7.lean`, `lean/KPSMod3_1_7.lean` |
| R12 | Auxiliary costs for the n = 7 programme: C([2x_1+x_2+…+x_5 ≡ 0]) = 9; C([2x_1+…+x_5 ≡ 2]) = 10; C([2x_1+…+x_6 ≡ 0]) ≥ 12 and C([2x_1+…+x_6 ≡ 1]) ≥ 12 | **machine-verified** (chains at 9 / 10 verified; UNSAT at 8 DRAT; UNSAT at 9 as 176 DRAT-checked cubes + checked cover; UNSAT at 11 DRAT; all with gelim-list + first-use order on x_2..x_n) | `results/logs/h5r0_s9.log`, `h5r0_s8.log`, `h5r2_s10.log`, `results/cnf/h5r2_s9.cnf.cubes.tsv`, `h5r2_s9.cnf.cover.log`, `h7r0_s11.log`, `h7r1_s11.log` |
| R13 | C([2x_1+x_2+…+x_6 ≡ 0]) ∈ {12, 13} and C([2x_1+…+x_6 ≡ 1]) ∈ {12, 13, 14}: explicit chains of 13 resp. 14 (mod-3 remainder of x_2..x_6 by KPS blocks + a 2/3-gate output block on ¬x_1) | **machine-verified** upper bounds (Python + Lean kernel) | `results/h7-r0-13.chain`, `results/h7-r1-14.chain`, `lean/H7r0_13.lean`, `lean/H7r1_14.lean` |
| R14 | n = 7, r = 0, 1 at s = 15 (the last open cells of Knuth's conjecture at n = 7) | **open / in progress**: cube runs `gp_7_{0,1}_s15` (1236 depth-3 cubes each; 106 resp. 558 closed, 14 timeouts each) paused; the missing ingredient is the exact cost (12 or 13) of the 6-input functions [2x_1+x_2+…+x_6 ≡ r] (R12, R13), whose refutation runs at 12 (`h7r{0,1}_s12L`, 3899 cubes each, ≈13 % done at the time of writing, ~1 day each projected) are running. Nothing here is a result yet. | `results/cnf/gp_7_*_s15.cnf.cubes.tsv`, `results/cnf/h7r*_s12L.cnf.cubes.tsv` |
| R8 | C(h) = 10 for h = [2x_1+x_2+x_3+x_4+x_5 ≡ 1 (mod 3)] (needed by Lemma 4) | **machine-verified**: chain (Python + `verify_chain.py`), UNSAT at 8 (DRAT), UNSAT at 9 (264 cubes, each DRAT-checked, cover DRAT-checked) | `results/cnf/h2xs_5_s10.cnf.chain`, `results/cnf/h2xg_5_s8.cnf*`, `results/cnf/h2xs_5_s9.cnf.cubes.tsv`, `python3 code/cnc.py cover results/cnf/h2xs_5_s9.cnf results/cnf/h2xs_5_s9.cnf.cubes` |

## The trusted surface: what the CNF means

A reader who distrusts everything here needs to check only three things:
(i) the CNF produced by `encode_a.py` (≈120 lines) is unsatisfiable exactly
when no *constrained* normal chain of length s computes the target (the
clauses are Knuth's, answer 477/478, reproduced to the clause count);
(ii) the DRAT proofs check with drat-trim (or cake_lpr) — that removes the
solver from the trusted base; (iii) the Lemma below, which says every
minimum-length chain can be brought into the constrained form, so UNSAT for
every s ≤ 12 implies C ≥ 13.

**Lemma (symmetry breaking is sound for minimum chains).** Let f be a normal
function depending on all n variables, invariant under all permutations of
the inputs (MOD3 is), with C(f) = c. Then there is a normal chain of cost c
computing f at its LAST step such that
 (a) every op is one of the five nontrivial normal ops (∧, ∧̄, ̄∧, ⊕, ∨);
 (b) every step is an operand of a later step or is the output;
 (c) no step i' = x_j ∘ x_i or x_k ∘ x_i where x_i = x_j ∘' x_k ("no reapply");
 (d) for consecutive steps i, i+1 where i+1 does not read i, pair(i) ≤ pair(i+1)
     in colex order ((j,k) < (j',k') iff k<k' or (k=k' and j<j'));
 (e) inputs are first used in the order x1, x2, …, xn (first use of x_q is at
     a step no earlier than the first use of x_{q−1});
 (f) no two steps have the same truth table and no step equals an input.
*Proof.* Take any minimum chain. (a),(b),(f): a step that is constant, a
projection, a duplicate of an earlier step/input, or unused can be deleted
(re-pointing its consumers; a negated projection is absorbed into the
consumer's op, which keeps the chain normal because f(0)=0 forces the final
op to absorb it too) — contradicting minimality; so all minimum chains satisfy
(a),(b),(f), and the last step is the output. (c): replace x_i' = x_j ∘ x_i by
x_i' = x_j ∘'' x_k (a function of the same two operands); length unchanged, so
still minimum, so (b) still holds; the sum of operand indices strictly
decreases, so iterating terminates. (d),(e): among all chains obtained from
this one by relabelling inputs (allowed by symmetry of f) and by re-ordering
steps topologically, take one whose sequence of operand pairs is
lexicographically minimal (pairs compared in colex order). If (d) failed at i,
swapping steps i and i+1 would decrease the sequence at position i; if (e)
failed, swapping the labels of the offending input with the smallest not-yet-
used label would decrease the sequence at the first step where it appears
(earlier steps do not mention either label). None of these operations breaks
(a),(b),(c),(f). ∎

Consequence: if the constrained formula is UNSAT for s = 1, …, 12 then
C(MOD3,1_6) ≥ 13. Note the constrained formula is *not* monotone in s (padding
is forbidden by (b)), so each s is a separate theorem.

**Lemma 2 (gate elimination ⇒ fanout bound).** Let a chain of cost s compute
f = MOD3,1_6, and let x_j be an input read by φ_j steps. Substituting x_j := 1
turns every step reading x_j into a constant or a (possibly negated) copy of its
other operand; deleting those steps (absorbing negations into consumers, which
B2 allows, and deleting any further steps that become unary or unused) leaves
a chain of cost ≤ s − φ_j computing ±MOD3,0_5 on the other five inputs. Hence
**φ_j ≤ s − C(MOD3,0_5) = s − 10** for every j (and φ_j ≥ 1 since f depends on
x_j). In particular: s ≤ 10 is impossible (φ_j ≤ 0); s = 11 forces φ_j = 1 for
all j; s = 12 forces φ_j ∈ {1,2}. Substituting x_j := 0 gives the weaker
φ_j ≤ s − C(MOD3,1_5) = s − 9. The same argument at n = 5 uses the n = 4 values
(φ_j ≤ s − 7 for r=0 via x_j:=0, φ_j ≤ s − 7 for r=1,2 via x_j:=1), and at n = 4
the n = 3 values; every value used is re-proved here with a DRAT certificate,
so the inductive chain of lemmas is machine-checked at every level. ∎

**Lemma 2′ (no collapse at the tight level).** In a chain satisfying (b) and (c)
of the Lemma above, if φ_j = s − 10 exactly, then no step reading x_j may become
*constant* under x_j := 1. Proof: let g = x_j ∘ y collapse to a constant. g is
not the output (MOD3,0_5 is not constant), so by (b) it has a consumer h; by
(c) h does not read x_j, so h ∉ {steps reading x_j}; h now reads a constant,
becomes unary, and is deleted too. The surviving chain has ≤ s − φ_j − 1 = 9
steps and computes ±MOD3,0_5, contradicting C(MOD3,0_5) = 10. Concretely, for
x_i = x_j ∘ y (x_j first operand) the op must have f10 ≠ f11; for x_i = y ∘ x_j
it must have f01 ≠ f11. ∎ (Without (c), the consumer of g could be g' = x_j ∘' g,
which is already among the deleted steps, and the lemma would be false.)

*Bookkeeping of the elimination, for both lemmas.* Process steps in order after
the substitution; a step is *alive* if both its operands are alive steps or
untouched inputs (its op is adjusted to absorb any negations, which B2 permits);
a step one of whose operands became a constant, or whose two operands became the
same literal, is replaced by a literal/constant and is *deleted*; unused steps
are deleted. The alive steps form a chain; the output is an alive step up to
complement (it cannot be an input or a constant), and alive ≤ s − (deleted).
Every step reading x_j is deleted, which gives Lemma 2; the extra deleted
consumer gives Lemma 2′.

**Lemma 3 (single-substitution gate-elimination count).** Fix an input x_j and
c ∈ {0,1}. Define, for the chain after substituting x_j := c, the sets
  K0/K1 = steps that become the constant 0/1 (a step reading x_j whose op has
  f(c,·) constant; a step one of whose operands is a constant step and whose op
  is constant in that argument; a step both of whose operands are constants),
  D = steps reading x_j ∪ K0 ∪ K1 ∪ steps reading a step of K0 ∪ K1.
Every step in D is deleted in the bookkeeping above, so |D| ≤ s − C(f|x_j:=c).
For f = MOD3,1_6: |D| ≤ s − 9 for c = 0 and |D| ≤ s − 10 for c = 1. (D is an
under-approximation of the deleted set — e.g. it ignores steps whose two
operands merge into one literal — which only weakens the constraint, so the
clause group is sound.) This subsumes Lemmas 2 and 2′ and several further hand
cases (a fanout-2 input must feed an XOR; a collapsing gate of a fanout-1 input
has fanout 1; …) that would otherwise have to be proved one by one. ∎
It is encoded (`--gelim cost0:cost1`) with auxiliary variables D_i, Z_i, O_i per
(j, c, step) and a sequential counter, all clauses in the "implied-by" direction
so that a genuine chain always yields a satisfying extension.

**Lemma 4 (pair substitution).** For two inputs x_a, x_b substitute x_a := x_b.
A step reading exactly {x_a, x_b} becomes unary (deleted), and is the constant 0
iff its op has f11 = 0; constants propagate as in Lemma 3 (only the constant 0
can arise, since all ops are normal). The surviving chain computes the 5-input
function h(x_b, rest) = [2x_b + Σrest ≡ 1 (mod 3)], so #deleted ≤ s − C(h).
**C(h) = 10, machine-verified** (row R8): C(h) ≤ 10 by an explicit chain
(`results/cnf/h2xs_5_s10.cnf.chain`, verified); C(h) ≥ 9 by UNSAT at s = 8
(`h2xg_5_s8`, DRAT); C(h) ≥ 10 by UNSAT at s = 9, run as 264 cubes (each DRAT-
checked) with a DRAT-checked cube-cover proof (`results/cnf/h2xs_5_s9.cnf.cubes*`).
The s = 9 formula used (i) first-use ordering among x_2..x_5 only (h is symmetric
in those; Lemma 1's lex-min argument applies verbatim to the subgroup S_4), and
(ii) Lemma 3 with residue costs 7:6 for x_1 (MOD3,1_4, MOD3,2_4) and 4:4 for
x_2..x_5 — the true residue costs there are 6 and 7 ([2x_1+y_1+y_2+y_3 ≡ 1], ≡ 0;
exhaustive enumerator), so 4:4 is a *weaker*, still sound, constraint. The clause
group `--gelim-pair COST` is sound for any COST ≤ C(h) = 10. Its effect is
dramatic on the hard cubes: the six slowest cubes of the s = 12 run (731 s,
495 s, 450 s, 393 s, 387 s, 383 s) all close in under a second with it. This
is the lemma that makes the structure "XOR of two inputs" cheap: if C(h) = 10,
an XOR step on two inputs has fanout exactly 1.
Validation: on the anchors the residue costs were computed *exhaustively* by
`enum_chains` (n=4: [2x_1+x_2+x_3+x_4 ≡ r] costs 7, 6, 7; n=3: 4, 4, 3), and every
SAT anchor stays SAT with the group.

All four lemma groups are switchable clause groups (`--fanout-max K`,
`--noncollapse c:K`, `--gelim c0:c1`) and were validated on every anchor cell
(all SAT cells remain SAT with the bounds; UNSAT cells remain UNSAT). They
turned (5,1,8) from 65 s into 0.3 s and (6,1,11) into a 166-second (fanout
only) / 0.6-second (fanout + no-collapse) DRAT-checked theorem.

## The s = 12 run

Formula: `encode_a.py 6 12 mod3:1 --symin --lastout --fanout-max 2 --noncollapse 1:2 --gelim 9:10 --gelim-pair 10`
(5776 variables, 351 884 clauses; Lemmas 1–4; file `results/cnf/gp_6_1_s12.cnf`).
Cubes: all (operand pair, op-bits) choices of steps 7–10 that survive unit
propagation (`cnc.py cubes --depth 4`): 18 760 cubes. Solver cadical 2.1.3 per
cube with a DRAT proof, each proof checked by drat-trim before the cube was
recorded; 30 workers; 18 754 cubes closed within the 1800 s limit (353 091
cube-seconds ≈ 98 CPU-hours; median well under a second, max 1800 s); the 6
that timed out were split one step deeper (`cnc.py refine`, 220 sub-cubes, all
UNSAT, max 41 s, 2865 cube-seconds). Leaves = 18 754 + 220 (+74 duplicates from a
first partial refinement) cubes, all UNSAT+proof-ok (`code/assemble_leaves.py`).
Cover: the CNF "F ∧ ¬(leaf_1) ∧ … ∧ ¬(leaf_N)" was refuted by kissat and the DRAT
proof checked by drat-trim (`cnc.py cover`, record in `results/cnf/gp_6_1_s12.cnf.cover.ok`),
so F ⊨ ∨ leaves and F is unsatisfiable. With Lemmas 1–4, no normal chain of
12 steps computes MOD3,1_6; with R4, R5 and R1: **C(MOD3,1_6) = 13.**

Wall clock: the first attempts (Lemmas 1–3 only) were projected at 400–600
CPU-hours because cubes containing two XOR-of-inputs gates among steps 7–9 cost
~2 CPU-hours each; Lemma 4 (pair substitution, needing C(h) = 10, R8) collapsed
exactly those cubes (e.g. 731 s → 0.2 s), and finer cubes under Lemma 4 made the
whole run ~100 CPU-hours. Proof files for the cube runs are not kept (terabytes);
the per-cube drat-trim verdicts are in the TSVs and any cube can be regenerated
and re-checked from `code/` (base CNF + the cube's unit clauses).

## The n = 7 cells (in progress / partly done)

Formulas (all residue costs certified above): (7,0,15): `--symin --lastout --fanout-max 2
--noncollapse 1:2 --gelim 12:13 --gelim-pair 12` (x:=0 → MOD3,0_6 = 12 [R9], x:=1 →
MOD3,2_6 = 13 [R7], fanout ≤ 15−13, pair residue [2x_b+…≡0] ≥ 12 [R12]); (7,1,15):
`--fanout-max 2 --noncollapse 0:2 --gelim 13:12 --gelim-pair 12` (x:=0 → MOD3,1_6 = 13,
x:=1 → MOD3,0_6 = 12, pair residue ≥ 12). Depth-3 cubes: 1236 each; cadical per cube
with DRAT checked. Status: see R14. Also certified on the way: C([2x_1+2x_2+x_3+x_4+x_5 ≡ 2]) = 9,
the other two members of that family ≥ 9 (`results/logs/g5r*`), and the n = 4 costs of
[2x_1+2x_2+x_3+x_4 ≡ r] = 6, 7, 7 (exhaustive).

## The dependency tree of the lower bound

Every arrow is a machine-checked certificate (SAT chain verified / DRAT proof
checked); every box at the leaves is a plain encoding with no lemma clauses.

    C(MOD3,r_3) = 3,4,4 ──(plain, A+B+exhaustive)
    C(MOD3,r_4) = 7,7,6 ──(plain, A+B; exhaustive enumeration confirms <=6 sets)
      └─ Lemma 2 at n=5 ─► C(MOD3,0_5) >= 10  [fo_5_0_s9; also plain by B: B_m3_5_0_s9]
      └─ plain ────────► C(MOD3,1_5) >= 9   [m3_5_1_s8; also B]
      └─ Lemma 3 at n=5 (residues 7:6 for x_1; 4:4 <= true 6:7 for x_2..x_5, exhaustive)
           + first-use ordering on x_2..x_5 ─► C(h) >= 10 [h2xg_5_s8, h2xs_5_s9 cubes + cover]
    C(MOD3,0_5)=10, C(MOD3,1_5)=9 ─► Lemmas 2, 2′, 3 at n=6 (fanout <= s−10, gelim 9:10)
    C(h)=10 ─────────────────────► Lemma 4 at n=6 (gelim-pair 10)
    Lemma 1 (symmetry breaking, elementary, holds for every minimum chain)
      └─► s <= 10 impossible (Lemma 2); s = 11 UNSAT [fo_6_1_s11]; s = 12: cube run
          [gp_6_1_s12_d4: each cube DRAT-checked + cover proof]  ⇒  C(MOD3,1_6) = 13.

## Failed approaches

- **Plain Knuth encoding at s = 12** (Lemma 1 only): 5750 depth-3 cubes; the first
  cubes averaged 355 s with heavy tails; projected ≈ 40 h for s = 11 alone and far
  more for s = 12. Abandoned after 14 minutes (`results/logs/cnc-t61_s11.log`).
- **Fanout bound only** (Lemma 2) at s = 12: 1857 cubes; the cubes with XOR-of-
  inputs gates took up to 7200 s and several timed out; projected days. Killed.
- **Lemma 3 (gate-elimination count) without Lemma 4**: 1282 cubes, 7 timed out at
  7200 s, projection 400–600 CPU-hours. Killed once Lemma 4 was available.
- **Solver presets**: `cadical --unsat` solved one cell in 2.8 s where the default
  took 166 s — but took 111 s where the default took 33 s. Run-to-run variance on
  this family is large; only cube-and-conquer averages it out. kissat was 2–4×
  slower than cadical on every n ≥ 5 UNSAT cell here.
- **`--distinct` (no two steps with equal truth tables)**: no measurable effect.
- **Refinement alone** (depth 3 → 4 under Lemma 3): break-even (≈ 2 CPU-h per parent
  cube either way); refinement paid off only in combination with Lemma 4.
- **Cost-9 version of Lemma 4** (sound before C(h) = 10 was proved): much weaker
  than cost 10 (cube 11: 534 s vs 0 s); the exact residue cost matters.
- One self-inflicted loss: two `pkill -f` patterns matched the shell that issued
  them and killed in-flight runs; recorded so the next person uses `[c]haracter`
  class patterns.

## What is new, and what is quoted

- **New and independently checkable:** the value C(MOD3,1_6) = C(MOD3,2_6) = 13
  (R7, with R1, R4, R5), closing the n = 6 case of Knuth's conjecture; the value
  C(h) = 10 (R8); the DRAT/Lean certificate chain; the exhaustive-enumeration
  confirmation of Knuth's Table 1 and of the n = 4 MOD3 values; the
  two-encoding cross-validation of Knuth's n ≤ 5 values.
- **New as a statement, from quoted ingredients:** Lemma 1 assembles Knuth's
  answer-478 remarks into one proved statement; Lemmas 2–4 are the classical
  gate-elimination idea (Stockmeyer, Schnorr, Zwick, …) turned into *exact*
  clause groups over known residue costs — not new as a technique, but to our
  knowledge not previously combined with the SAT encoding for this problem.
- **Elementary:** all four lemmas.
- **Not ours:** the encoding (Kojevnikov–Kulikov–Yaroslavtsev 2009; Knuth
  477/478), the 13-step construction (KPS), Biere's 12-step chain, all anchor
  values (Knuth), cube-and-conquer (Heule–Kullmann–Biere), drat-trim.
- **Novelty caveat:** we did not search the literature for a prior resolution
  beyond the 2026-08-22 web check (Knuth's Vol 4B errata through 2026-04,
  KPS 2022, the 2025 "Simplifier" paper, a Feb-2026 gate-elimination preprint),
  repeated on 2026-08-23 together with Knuth's "Recent News" page (no mention of
  mod 3, Boolean chains, or exercise 480). The widely reported 2026 "Knuth
  conjecture solved by AI" is a *different* problem — Knuth's *Claude's Cycles*
  (Hamiltonian decompositions of the directed torus D_3(m), odd m; see
  `problems/directed-torus-even-modulus` in this repo) — not the mod-3
  circuit-size conjecture treated here.

## Reproduction

```bash
cd problems/mod3-circuit-size
python3 code/verify_chain.py results/kps-mod3-1-6.chain     # VALID, cost 13
python3 code/verify_chain.py results/knuth-mod3-0-6.chain   # VALID, cost 12 (complement)
~/.elan/bin/lean lean/KPSMod3_1_6.lean && ~/.elan/bin/lean lean/BiereMod3_0_6.lean   # ~3 s each, kernel decide
gcc -O3 -o code/enum_chains code/enum_chains.c && code/enum_chains 4 6   # 24 s; Knuth Table 1 counts
python3 code/encode_a.py 3 4 maj xor --no-colex 2>&1 >/dev/null          # vars=82 clauses=942 (Knuth N4, M4)
python3 code/batch.py results/anchors-A.cells results/anchors-A.tsv --jobs 8   # re-runs every anchor cell
```
Versions: Python 3.14, kissat 4.0.3, cadical 2.1.3, drat-trim (marijnheule/drat-trim, built 2026-08-22), Lean 4.9.0.

## Artifact hashes

See `HASHES.txt` (to be generated at the end).

## Open

1. The (6,0,11) anchor (Knuth: C(MOD3,0_6) = 12) was not reproduced in this
   session: both the plain (kissat) and the Lemma-2 (cadical) runs were still
   running after 12 hours when this was written; the SAT half (Biere's chain, and
   our own `fo_6_0_s12`) is verified. Knuth's value is not used anywhere in the
   proof of R7.
2. Knuth's conjecture at n = 7: r = 2 is now closed (R10); r = 0, 1 are pinned to
   {15, 16} (R11), conjectured 16. Refuting s = 15 there is the analogue of the
   s = 12 run here (fanout slack 2) and needs a Lemma-4 analogue, i.e. the exact
   costs of the 6-input functions [2x_1 + x_2+…+x_6 ≡ r]; those are themselves
   n = 6 problems of the size solved in R7. Started (see `results/logs/h*_6_*`).
3. A formally verified checker (cake_lpr) could replace drat-trim; not done.