cert-machine · audit · five Graffiti.pc conjectures, 2009–2010
Written on the Wall II: five counterexamples, decided
On 2026-10-14 one account filed sixty issues and twenty-three pull requests on DeepMind's formal-conjectures repository, each a Written-on-the-Wall-II conjecture of DeLaViña's Graffiti.pc with a Lean statement, a "research solved" tag and a disproof manuscript. Five of them — three on total domination in trees, two on 2-domination in connected graphs — come with explicit witness graphs. All five witnesses are rebuilt here from the author's own Lean tables and decided in exact arithmetic from the archive's definitions: every one refutes its conjecture, by the margins the author states. Two notes on the statements and one on provenance: the author's fork had rewritten the cited commits before this page was built.
The conjectures: WOWII 353, 360, 373 (18 Feb 2009) and 395b, 396 (Jan 2010), open in DeLaViña's archive (cms.uhd.edu/faculty/delavinae/research/wowII), read from the Internet Archive's 2010 and 2016 snapshots of open.html and the live definitions file; the claims: issues #7304, #7305, #7306, #7308, #7330 and PRs #7310, #7321, #7322, #7320, #7337 on google-deepmind/formal-conjectures (author RhudeJJJJ, self-identified Jonas J. Gebendorfer, Codex-assisted; sorry-proofs with a formal_proof link to the author's fork). Every byte pinned by sha256 in corpus/wowii/PINS.json; no Lean built, no claimant code run. Pre-registered in corpus/wowii/preregistration.json. What is decided: that each graph is a counterexample to the archive's inequality. Not decided: the manuscripts' infinite families, or whether the Lean proofs in the fork compile.
tl;dr
- The finding. All five graphs refute their conjectures. 353: γ_t = 10 against a right side of 21/2 on a 25-vertex tree. 360: γ_t = 6 against 961/160 (and 641/80 without the ½ the 2026 archive copy dropped — either way). 373: γ_t = 12 against 19676/1639 on 150 vertices. 396: γ₂ = 12 against 10 on six bridged cliques. 395b: γ₂ = 6 against 5 on three. Two notes on the Lean statements: 395b adds a hypothesis the archive does not have (V ∖ A nonempty — needed because δ(G[V∖A]) is undefined on regular graphs; it weakens the universal, and the witness satisfies it); 396 writes dd_mode as the number of modes, which definition 45 leaves undefined for a unique mode — moot here, the witness has two. Provenance: the five formal_proof links 404 since ~20:45 UTC on 10-15 and the fork's main no longer carries the files; the copies decided here were fetched at 17:14 UTC and are pinned.
- The mechanism. Standard library, exact: γ_t by a tree dynamic programme sandwiched by the author's explicit sets (upper) and vertices with pairwise disjoint open neighbourhoods (lower); γ₂ by exhaustion over 2¹⁵ subsets, or on 39 vertices by the private-vertex argument — each clique keeps two vertices with no outside neighbour, forcing two per clique into every 2-dominating set — met by an explicit set; components, eccentricities, centres, periphery, modes and averages as rationals. The DP equals brute force on 25 random trees.
- Check it. python3 -I tools/run-wowii-ledger.py · python3 -I instruments/wowii/battery.py — 19 checks, 7 red controls.
conjectures refuted
5 of 5
Open in the archive since 2009–2010; every witness as the author built it.
largest witness
150
Vertices, for 373; γ_t = 12 against 19676/1639.
margin
1
The clique graphs beat their bounds by two (396) and one (395b); the trees by ½, 1/160 and 8/1639.
statement notes
2
A hypothesis added to 395b; dd_mode on a unique mode in 396. Neither touches the witnesses.
§1 · the five
Each inequality on its witness
| WOWII | the inequality | witness | left side | right side | verdict |
|---|
| 353 | for a tree T on n > 2 vertices | 25 vertices, 24 edges, a tree | 10 | 21/2 | CERTIFIED |
| 360 | for a tree T on n > 2 vertices | 41 vertices, 40 edges, a tree | 6 | 961/160 | CERTIFIED |
| 373 | for a tree T on n > 2 vertices | 150 vertices, 149 edges, a tree | 12 | 19676/1639 | CERTIFIED |
| 396 | for a connected graph on n > 2 vertices | 39 vertices, 121 edges, connected | 12 | 10 | CERTIFIED |
| 395b | for a connected graph on n > 2 vertices | 15 vertices, 38 edges, connected | 6 | 5 | CERTIFIED |
A CERTIFIED row says the graph is a counterexample: the inequality fails on it by exact arithmetic. Left sides are domination numbers decided exactly (the DP, the exhaustion, or the private-vertex argument met by a set); right sides are the archive's expressions as rationals.
§2 · how each side was decided
The deciders, row by row
- WOWII 353. gamma_t by exact tree DP = 10 (the claimant's set of 10 is total dominating; 9 support vertices force >= 9); c(T[D_2]) = 9, k_M = 3, so the right side is 21/2
- WOWII 360. gamma_t by exact tree DP = 6 (the set {1,2,3,6,7,8} is total dominating; six vertices with pairwise disjoint open neighbourhoods give >= 6); c(T[S u L]) = 4, centre [4, 5], dist_avg(C,V) = 321/80, right side 961/160; without the half (the 2026 archive copy lost the byte) the right side is 641/80 and the inequality fails too
- WOWII 373. gamma_t by exact tree DP = 12 (the 12-vertex set is total dominating); periphery of 11 vertices at eccentricity 23, transmission sum 29514 over 1639 positive pairs, dist_avg = 29514/1639, (2/3) of it = 19676/1639
- WOWII 396. every clique keeps >= 2 vertices with no outside neighbour, so a 2-dominating set has >= 2 in each of the 6 cliques (12); two per clique 2-dominate (12): gamma_2 = 12. Degree frequencies {3: 3, 4: 4, 5: 6, 6: 8, 7: 8, 8: 7, 9: 3}, modes [6, 7] (dd_mode = 2), |M| = 8, boundary edges 0: right side 10
- WOWII 395b. gamma_2 = 6 by exhaustion over all 2^15 subsets (a minimum set: [0, 1, 4, 5, 9, 10]); modes [6], |M| = 4, minimum degree 3, delta(G[V - A]) = 1, vertices of degree < 3: 0; right side 5
§3 · the statements
The Lean against the archive
- WOWII 353. the Lean (PR #7310) states c(T[D_2]) + k_M/2 <= gamma_t over rationals with largestComponentOrder = sup of component orders: the archive's statement
- WOWII 360. the Lean (PR #7321) ranges centres over minimum eccentricity and averages over |C|(n-1): definition 38; the half is in the 2010 and 2016 archive snapshots (byte 0xBD) and dropped from the 2026 copy
- WOWII 373. the Lean (PR #7322): periphery = maximum eccentricity, denominator |B|(n-1): definition 95
- WOWII 396. the Lean (PR #7320) writes |M| as maximumFrequency (equal: M is the class of the smallest mode, whose size is the maximum frequency) and dd_mode as the number of modes; definition 45 leaves dd_mode undefined for a unique mode — the witness has two
- WOWII 395b. the Lean (PR #7337) adds the hypothesis (remaining G).Nonempty — the archive's delta(G[V - A]) is undefined on regular graphs — which weakens the universal statement; the witness satisfies it (minimum degree 3, twelve vertices above it)
On 360 the archive's own copies disagree: the Internet Archive's 2010 and 2016 snapshots carry "½ · dist_avg(C,V)" as the byte 0xBD; the 2026 copy the author first read shows a blank there. The ½ is original. The witness refutes both readings, so nothing turns on it.
§4 · limits
What is not decided here
- The manuscripts' families. Each paper claims infinitely many counterexamples (every order ≥ 150 for 373; 39r vertices for 396); only the one explicit witness of each is decided.
- The fork's Lean. Whether the author's proofs compile is not checked; the witnesses are read from them as data. Their statements were compared with the archive by reading.
- Priority and the sixty issues. The other fifty-five issues and eighteen PRs of the same account are not examined; nothing is said about them.
- Same-author second implementation. The DP and the brute force are the same author's; the sandwich certificates (the author's sets and the disjoint-neighbourhood lower bounds) are the independent leg.