A Proof of Graffiti 290 · July 23, 2026 · revised October 7, 2026 · Companion: Graffiti 292
python -m pip install sympy networkx numpy
python verify_290_symbolic.py
python verify_290_small_cases.py
python independent_check_284_290.py
python battery_290.py
# Lean 4 proof (in lean/)
lake exe cache get
lake build| File | Purpose |
|---|---|
| manuscript-graffiti-290.md | Markdown manuscript with full derivations |
| verify_290_symbolic.py · output | Symbolic reduction: (t+1)²Q(t) factorization, Q(u+5) coefficient positivity, exact endpoints n=5,6 |
| verify_290_small_cases.py · output | Exhaustive exact small-case battery (34 connected girth ≥ 5 graphs, 2 ≤ n ≤ 7) + named-graph margins |
| independent_check_284_290.py · output | Independent reimplementation: pentagon/pentagram HS, LCF cages, 60 random trees, 40 girth-pruned graphs (shared with 284 note) |
| battery_290.py · output | Uniform bound (§2.5): exact checks of every inequality on 345 girth ≥ 5 graphs |
| lean/Graffiti/Graffiti290.lean · Basic.lean · Gravity.lean | Lean 4 proof (§2.6); the full project is in lean/ and at agnt-gg/graffiti-lean |
| claim-ledger.json | Claim-by-claim evidence map (covers 290 proof + 284 refutation verification + 295 attack state) |
| wow-p79-bot.png | Primary source: rendered scan of the WoW page 79 (conjecture 290 statement) |
| wow-p80-top.png | Primary source: rendered scan of the WoW page 80 (conjectures 292, 295) |
| SHA256SUMS.txt | SHA-256 integrity ledger |
| Battery | Result |
|---|---|
| 1. Named-graph battery (Petersen, HS, Heawood, Pappus, Desargues, Möbius–Kantor, dodecahedron, cycles, paths, spiders) | PASS |
| 2. Symbolic reduction (SymPy) | PASS |
| 3. Exhaustive exact small cases (34 graphs, Sturm root counts) | PASS |
| 4. Independent reimplementation (from-scratch, LCF cages, random samples) | PASS |
| 5. Uniform bound (345 graphs, exact rational sums) | PASS |
| 6. Lean 4 formal proof | PASS (standard axioms only) |
