Graffiti 292 — Reproducibility Archive

A Proof of Graffiti 292 · July 23, 2026 · revised October 7, 2026

Scope. These artifacts verify the proof of Graffiti 292 under the gravity normalization documented in the source corpus. Novelty is provisional; priority is not claimed.

Replay

python -m pip install sympy networkx numpy
python attack_graffiti_292.py
python verify_symbolic_292.py
python verify_small_cases_exact.py
python verify_independent_292.py
python verify_twopath_292.py

# Lean 4 proof: put the four Lean files below in one folder, then
lake exe cache get
lake build

Files

File	Purpose
manuscript-graffiti-292.pdf	Typeset proof (XeLaTeX, 2 pages)
manuscript-graffiti-292.tex	LaTeX source
manuscript-graffiti-292.md	Markdown manuscript with full derivations
attack_graffiti_292.py · output	Named-graph battery: exact gravity means, spectra, atlas ≤ 7
verify_symbolic_292.py · output	Symbolic reduction: cleared polynomial, endpoint, shifted coefficients
verify_small_cases_exact.py · output	Exact characteristic polynomials and rational root isolation, 35 atlas cases
verify_independent_292.py · output	From-scratch independent reimplementation: 18,686 exhaustive graphs, analytic bound, four cages
verify_twopath_292.py · output	Stronger uniform bound (§2.5): cherry count, exact atlas and cages
Graffiti292.lean	Lean 4 proof of the §2.5 argument (§2.6)
lakefile.toml · lake-manifest.json · lean-toolchain	Lean project files: Lean v4.33.1 and Mathlib v4.33.1, pinned
claim-ledger.json	Claim-by-claim evidence map
wow-july2004.pdf	Primary source scan (Written on the Wall)
page80-detail.txt	OCR of page 80 (conjecture 292 statement)
SHA256SUMS.txt	SHA-256 integrity ledger

Verification outcomes

Battery	Result
Named-graph evaluator	PASS
Symbolic reduction	PASS
Exact small-case enumeration	PASS (35 cases)
Independent reimplementation	PASS (18,686 graphs)
Uniform bound (§2.5)	PASS
Lean 4 formal proof (§2.6)	PASS (standard axioms only)