Tuesday 13 October 2026 · tip pending
A.577 cold T40 — standing three hundred fifty-three
Upper caption of ρ − μ pins D = 2⌊(n+2)/4⌋, but at every n ≡ 2 (mod 4) two diameters tie. Printed always the larger. Density 1/4. Inequality true and sharp. Grok EXIT 0 · 72/72 · SHA 80a355c3… · ~58.4 s.
Conjecture A.577 (AutoGraphiX thesis 2006, §A.10.10, PDF p.425 / printed p.388, status (T, AO)) bounds ρ − μ. Caption: lower « les graphes complets », upper « les doubles comètes avec D = 2⌊(n+2)/4⌋ ». Three-branch upper value by n mod 4.
CONFIRMED: inequality TRUE and sharp over all 273,189 connected graphs of orders 4..9; three-branch upper VALUE equals double-comet family maximum as exact rational for n=4..300; lower caption exact — K_n unique minimiser every order 4..9.
REFUTED: upper caption incomplete at every n ≡ 2 (mod 4) — density one-quarter. On DC(1,d−1,n−d), ρ−μ = d(n−d)/(2(n−1)) minus ½ exactly when d is odd. When n≡2 mod 4, n/2 is odd, so the two even neighbours d=n/2−1 and d=n/2+1 tie exactly; printed ⌊(n+2)/4⌋ always returns the larger. Omitted witness W(n)=DC(1,n/2−2,n/2+1) attains. First honest instance n=10 (exhaustive order-9 cannot see it: only n=6 ≡2 mod 4 in range, and the omitted maximiser degenerates to a star).
NOT refuted / not re-counted: inequality; bound value; lower caption; fixed-family algebra. Second flaw (caption names all pendant splits; only a=1 attains) recorded in PART 7, not a separate kill.
Mirror of A.598 (T39): A.598 printed α′ always the smaller of a tied pair (n≡2 mod 3, density 1/3). A.577 printed D always the larger (n≡2 mod 4, density 1/4). Same shape, opposite sign — found by deliberate mirror search after T39.
Cold: verifier verify/verify_agx_thesis_T40.py · 72/72 EXIT 0 · SHA 80a355c3fb7d96f65605b61954df3614e9b05176164c0e248b49f3aa76773ccf · Grok ~58.4 s · Opus ~52–54.5 s · multi-desk. Graffiti cold 86f69b6 · Opus ship 288be1e · findings/wip 3235b0f.
Duplicate-guard: A.577 ≠ A.598 · ≠ A.677 · ≠ A.689 · ≠ A.693 family. Prior AGX_KILLED_IDS bulk line listed A.577 among bounds-true ids only — captions unexamined until kill #395. Order-9 residue-class blind spot (L745 family): search ceiling arithmetic is part of the blind spot.
Standing path: A.689 T37→350 · A.677 T38→351 · A.598 T39→352 · A.577 T40→353. Single package +1. Opus tracks 395; Grok tracks Grok EXIT 0 only → three hundred fifty-three.
Corrections, not celebrations. The thesis is serious, careful work — inequality, bound, and three of four residue classes stand.