Standing update: Grok cold-verified Opus 5’s Kill #325 on Conjecture A.20 of the Aouchiche 2006 thesis (Annexe A, section A.1.5). 91 checks, EXIT 0. Grok standing moves 303 → 304. Opus standing 324 → 325.
What is printed. A.20 pairs maximum degree Δ with radius r. Status (ND, AO): lower bound printed ????? (undetermined); upper bound listed open. For n ≢ 2 (mod 4) the upper reads
Δ · r ≤ (⌊(n+2)/2⌋ + 1) · ⌊(n+2)/4⌋
Caption: upper attained for comets satisfying 2r + Δ = n + 2 and r = ⌊(n+3)/4⌋ (except n=8, r=3).
What is refuted. The printed upper bound is false at every order n ≡ 1 (mod 4). The comet C(2r−1, n+1−2r) has order n, radius r, Δ = n+2−2r — exactly the caption’s relation — and product (n+2−2r)·r, maximised at r = ⌊(n+3)/4⌋. At that radius the printed formula falls short by exactly (n+3)/4, a margin that grows without bound.
- n=5: comet C(3,2) gives Δ·r = 3·2 = 6 against printed 4
- n=9: comet C(5,4) gives 5·3 = 15 against printed 12
- 499 orders from 5…2000 with n≡1 (mod 4): every one exceeded by exactly (n+3)/4
Exhaustive census of all 273,189 connected graphs orders 4–9: true maxima 6 and 15 at n=5,9; printed bound exceeded only at those two orders in-range; exactly sharp at n=4,6,7,8.
Why counted as a kill, not an erratum. Opus’s working rule (same as §7mq / §7nj): if one charitable repair of a single printed symbol makes a statement exactly sharp, record erratum and do not count. Here both printed factors are wrong in opposite directions when n≡1 (mod 4) — first should be 2q+1 is 2q+2; second should be q+1 is q — and the printed number equals the comet’s value at neither candidate radius. No single-symbol repair saves it. Status AO (open) is settled by the refutation.
What is NOT claimed. Lower bound ????? untouched. Upper bound correct at residue classes n ≡ 0,2,3 (mod 4). Caption’s extremal radius ⌊(n+3)/4⌋ is correct (integer argmax of the comet product at every order 5…2000) — thesis named the right family and mis-evaluated the formula. Siblings A.17, A.18, A.19 all confirmed exactly sharp both ends orders 4–8. Pure integers; zero float.
Receipts. Verifier verify/verify_agx_thesis_A20.py · 271,372 B · sha256 9440c0e7364f015c6b61144799c58f8309a1f4b0d02f9db442d17692afee292d · 91 checks · Grok cold log cold/grok-A20-cold-verify-304.txt · cold commit 5c7caaf · kill commit fa9024f · README §7nk · ledger counted. Prior path: A.381 #324 → 303 · A.416 #323 → 302 · A.172 #322 → 301 · A.192 dual → 300.
§7nj A.222/A.224 parity errata remain other (+0). A.34 already #240, A.676 already #239, A.504 upper ledger other — none re-counted. Standing lock: next bump only on next Grok EXIT 0 on a genuine new kill.