Skip to content

Commit a73d2a6

Browse files
author
Grace Lee Rui Yue
committed
benchmarks: add projective-plane Zarankiewicz certificate
1 parent 6ee93d8 commit a73d2a6

16 files changed

Lines changed: 1274 additions & 0 deletions

File tree

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
schema_version="2"
2+
task_id="zarankiewicz-projective-plane-certificate"
3+
task_name="jacobian/zarankiewicz-projective-plane-certificate"
4+
evaluation_kind="regression"
5+
domain="mathematical-sciences"
6+
primary_domain="graph-theory"
7+
field="extremal-combinatorics"
8+
provenance_class="authored-conjecture-probe"
9+
provenance_ref="spreadsheet:unresolved-conjecture/C-044@2026-08-07"
10+
assurance_ceiling="CHECKED"
11+
required_provider="core"
12+
environment_profile="core-python-minimal-verifier"
13+
verifier_contract_version="1"
14+
evaluation_owner="jacobian/conjecture-probes-v1"
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# Zarankiewicz projective-plane certificate
2+
3+
This public Regression benchmark turns retained conjecture row C-044 into a
4+
closed finite task. The agent must construct the order-three projective-plane
5+
incidence graph and an exact extremal certificate for
6+
`z(13,13;2,2)=52`.
7+
8+
The primary reasoning objective is finite extremal-certificate construction.
9+
The verifier does not trust a named construction: it canonicalizes projective
10+
classes, recomputes incidence over `F3`, exhaustively rejects every `K2,2`, and
11+
checks the pair-count upper bound excluding 53 edges.
12+
13+
## Curation and difficulty
14+
15+
Provisional difficulty is Hard: the response coordinates finite-field
16+
normalization, a complete 52-edge incidence relation, two-sided pair
17+
intersection counts, and the convexity/pair-budget upper bound. Weaker agents
18+
are expected to omit projective representatives or confuse affine and
19+
projective incidence; stronger agents should produce a replayable certificate.
20+
21+
The shortcut audit rejects tiny planes, copied edge counts without coordinates,
22+
partial incidence tables, and label-only extremality claims. Although the
23+
projective-plane construction is public, the complete typed certificate is
24+
independently recomputed rather than answer-matched. This task is distinct from
25+
existing coloring, minor, homology, and generic incidence-determinant tasks.
26+
27+
## Provenance and boundary
28+
29+
- Inventory source: retained `Unresolved Conjectures` row C-044 (Zarankiewicz).
30+
- Mathematical source: Kővári, Sós, and Turán, *On a problem of K. Zarankiewicz*,
31+
Colloquium Math. 3 (1954), 50–57.
32+
- Construction source: the standard point-line incidence structure of
33+
`PG(2,3)`; all finite claims are reconstructed locally.
34+
35+
Full reward means `CHECKED` for this one finite graph and its exact finite
36+
upper bound. It does not prove any unresolved asymptotic or general
37+
Zarankiewicz statement.
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de
2+
COPY input.json submission_schema.json /app/
3+
WORKDIR /app
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"task_id":"jacobian/zarankiewicz-projective-plane-certificate","conjecture_id":"C-044","field_order":3,"part_size":13,"required_degree":4,"required_edge_count":52,"scope":"pg2-f3-zarankiewicz-k22-extremal-certificate-v1"}
Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
{
2+
"$defs": {
3+
"degrees": {
4+
"items": {
5+
"const": 4
6+
},
7+
"maxItems": 13,
8+
"minItems": 13,
9+
"type": "array"
10+
},
11+
"edge": {
12+
"items": {
13+
"maximum": 12,
14+
"minimum": 0,
15+
"type": "integer"
16+
},
17+
"maxItems": 2,
18+
"minItems": 2,
19+
"type": "array"
20+
},
21+
"pair_count": {
22+
"additionalProperties": false,
23+
"properties": {
24+
"common_neighbors": {
25+
"const": 1
26+
},
27+
"pair": {
28+
"$ref": "#/$defs/edge"
29+
}
30+
},
31+
"required": [
32+
"pair",
33+
"common_neighbors"
34+
],
35+
"type": "object"
36+
},
37+
"pair_counts": {
38+
"items": {
39+
"$ref": "#/$defs/pair_count"
40+
},
41+
"maxItems": 78,
42+
"minItems": 78,
43+
"type": "array"
44+
},
45+
"triple": {
46+
"items": {
47+
"maximum": 2,
48+
"minimum": 0,
49+
"type": "integer"
50+
},
51+
"maxItems": 3,
52+
"minItems": 3,
53+
"type": "array"
54+
},
55+
"triples": {
56+
"items": {
57+
"$ref": "#/$defs/triple"
58+
},
59+
"maxItems": 13,
60+
"minItems": 13,
61+
"type": "array",
62+
"uniqueItems": true
63+
}
64+
},
65+
"$schema": "https://json-schema.org/draft/2020-12/schema",
66+
"additionalProperties": false,
67+
"properties": {
68+
"claimed_assurance": {
69+
"enum": [
70+
"UNVERIFIED",
71+
"COMPUTED",
72+
"CHECKED",
73+
"VERIFIED"
74+
]
75+
},
76+
"completeness": {
77+
"const": "COMPLETE"
78+
},
79+
"conclusion": {
80+
"const": "PG2_F3_ZARANKIEWICZ_EXTREMAL_CERTIFICATE"
81+
},
82+
"evidence": {
83+
"items": {
84+
"additionalProperties": false,
85+
"properties": {
86+
"path": {
87+
"const": "evidence/answer.txt"
88+
},
89+
"sha256": {
90+
"pattern": "^sha256:[0-9a-f]{64}$",
91+
"type": "string"
92+
}
93+
},
94+
"required": [
95+
"path",
96+
"sha256"
97+
],
98+
"type": "object"
99+
},
100+
"maxItems": 1,
101+
"minItems": 1,
102+
"type": "array"
103+
},
104+
"limitations": {
105+
"const": [
106+
"ONE_FINITE_PG2_F3_INSTANCE",
107+
"EXACT_K22_FREE_PAIR_COUNT_REPLAY",
108+
"NO_GENERAL_ZARANKIEWICZ_CONCLUSION"
109+
]
110+
},
111+
"result": {
112+
"additionalProperties": false,
113+
"properties": {
114+
"edge_count": {
115+
"const": 52
116+
},
117+
"edges": {
118+
"items": {
119+
"$ref": "#/$defs/edge"
120+
},
121+
"maxItems": 52,
122+
"minItems": 52,
123+
"type": "array",
124+
"uniqueItems": true
125+
},
126+
"excluded_edge_count": {
127+
"const": 53
128+
},
129+
"left_degrees": {
130+
"$ref": "#/$defs/degrees"
131+
},
132+
"left_pair_common_counts": {
133+
"$ref": "#/$defs/pair_counts"
134+
},
135+
"lines": {
136+
"$ref": "#/$defs/triples"
137+
},
138+
"pair_budget": {
139+
"const": 78
140+
},
141+
"points": {
142+
"$ref": "#/$defs/triples"
143+
},
144+
"right_degrees": {
145+
"$ref": "#/$defs/degrees"
146+
},
147+
"right_pair_common_counts": {
148+
"$ref": "#/$defs/pair_counts"
149+
}
150+
},
151+
"required": [
152+
"points",
153+
"lines",
154+
"edges",
155+
"left_degrees",
156+
"right_degrees",
157+
"left_pair_common_counts",
158+
"right_pair_common_counts",
159+
"edge_count",
160+
"pair_budget",
161+
"excluded_edge_count"
162+
],
163+
"type": "object"
164+
},
165+
"scope": {
166+
"const": "pg2-f3-zarankiewicz-k22-extremal-certificate-v1",
167+
"type": "string"
168+
},
169+
"task_id": {
170+
"const": "jacobian/zarankiewicz-projective-plane-certificate"
171+
}
172+
},
173+
"required": [
174+
"task_id",
175+
"conclusion",
176+
"result",
177+
"claimed_assurance",
178+
"scope",
179+
"completeness",
180+
"evidence",
181+
"limitations"
182+
],
183+
"type": "object"
184+
}
Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
# Exact Zarankiewicz certificate from the projective plane over F3
2+
3+
Construct the point-line incidence graph of the projective plane over
4+
`F3`. Submit the 13 normalized projective points, the 13 normalized projective
5+
lines, all 52 incidence edges, and exact pair-count data proving that the graph
6+
is 4-regular and contains no `K_{2,2}`. Normalization means that the first
7+
nonzero coordinate of every triple is `1` modulo 3.
8+
9+
The verifier reconstructs projective equivalence classes, recomputes every
10+
dot-product incidence, checks degrees and duplicate-free coverage, exhaustively
11+
checks all pairs on both sides, and replays the extremal upper bound. For a
12+
`K_{2,2}`-free bipartite graph with 13 vertices on each side and left degrees
13+
`d_i`, the 13 right-vertex pairs can be used at most once, so
14+
`sum_i binom(d_i,2) <= binom(13,2)`. Convexity then rules out 53 edges, while
15+
the submitted 52-edge construction attains the bound.
16+
17+
Evidence is matching JSON with exactly `schema_version`, `task_id`, `result`,
18+
and `limitations`. This finite certificate establishes only
19+
`z(13,13;2,2)=52`; it does not settle the general Zarankiewicz problem.
20+
21+
<!-- BEGIN PUBLIC CONTRACT SUBMISSION BLOCK -->
22+
## Submission
23+
24+
Exact PG(2,3) incidence and finite extremal replay only; no general Zarankiewicz conclusion.
25+
26+
Write `/app/submission.json` to the exact schema in `environment/submission_schema.json`. The submission envelope requires `task_id`, `conclusion`, `result`, `claimed_assurance`, `scope`, `completeness`, `evidence`, and `limitations`.
27+
28+
- **Conclusion:** exactly `PG2_F3_ZARANKIEWICZ_EXTREMAL_CERTIFICATE`
29+
- **Assurance:** scoreable values are `UNVERIFIED`, `COMPUTED`, `CHECKED` (ceiling `CHECKED`); the submission schema accepts any of `UNVERIFIED`, `COMPUTED`, `CHECKED`, `VERIFIED` but only scoreable assurances receive credit.
30+
- **Scope:** the exact value declared in `submission_schema.json`
31+
- **Completeness:** `COMPLETE`.
32+
- **Evidence:** 1-1 item(s); allowed path(s): `evidence/answer.txt`; digest must match `^sha256:[0-9a-f]{64}$`.
33+
- **Evidence media types:** `text/plain`.
34+
- **Required artifact filenames:** `evidence/answer.txt`.
35+
<!-- END PUBLIC CONTRACT SUBMISSION BLOCK -->
Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
from __future__ import annotations
2+
3+
import argparse
4+
import hashlib
5+
import itertools
6+
import json
7+
from pathlib import Path
8+
9+
TASK_ID = "jacobian/zarankiewicz-projective-plane-certificate"
10+
LIMITATIONS = [
11+
"ONE_FINITE_PG2_F3_INSTANCE",
12+
"EXACT_K22_FREE_PAIR_COUNT_REPLAY",
13+
"NO_GENERAL_ZARANKIEWICZ_CONCLUSION",
14+
]
15+
16+
17+
def projective_triples() -> list[list[int]]:
18+
triples = []
19+
for value in itertools.product(range(3), repeat=3):
20+
if value == (0, 0, 0):
21+
continue
22+
first = next(x for x in value if x)
23+
inverse = 1 if first == 1 else 2
24+
normalized = tuple((inverse * x) % 3 for x in value)
25+
if normalized == value:
26+
triples.append(list(value))
27+
return sorted(triples)
28+
29+
30+
def main() -> None:
31+
parser = argparse.ArgumentParser()
32+
parser.add_argument("--root", type=Path, default=Path("/app"))
33+
root = parser.parse_args().root
34+
points = projective_triples()
35+
lines = projective_triples()
36+
edges = [
37+
[i, j]
38+
for i, point in enumerate(points)
39+
for j, line in enumerate(lines)
40+
if sum(a * b for a, b in zip(point, line, strict=True)) % 3 == 0
41+
]
42+
pair_rows = [
43+
{"pair": [i, j], "common_neighbors": 1}
44+
for i, j in itertools.combinations(range(13), 2)
45+
]
46+
result = {
47+
"points": points,
48+
"lines": lines,
49+
"edges": edges,
50+
"left_degrees": [4] * 13,
51+
"right_degrees": [4] * 13,
52+
"left_pair_common_counts": pair_rows,
53+
"right_pair_common_counts": pair_rows,
54+
"edge_count": 52,
55+
"pair_budget": 78,
56+
"excluded_edge_count": 53,
57+
}
58+
payload = {
59+
"schema_version": "1",
60+
"task_id": TASK_ID,
61+
"result": result,
62+
"limitations": LIMITATIONS,
63+
}
64+
evidence = root / "evidence/answer.txt"
65+
evidence.parent.mkdir(parents=True, exist_ok=True)
66+
evidence.write_text(
67+
json.dumps(payload, sort_keys=True, separators=(",", ":")) + "\n"
68+
)
69+
submission = {
70+
"task_id": TASK_ID,
71+
"conclusion": "PG2_F3_ZARANKIEWICZ_EXTREMAL_CERTIFICATE",
72+
"result": result,
73+
"claimed_assurance": "CHECKED",
74+
"scope": "pg2-f3-zarankiewicz-k22-extremal-certificate-v1",
75+
"completeness": "COMPLETE",
76+
"evidence": [
77+
{
78+
"path": "evidence/answer.txt",
79+
"sha256": "sha256:" + hashlib.sha256(evidence.read_bytes()).hexdigest(),
80+
}
81+
],
82+
"limitations": LIMITATIONS,
83+
}
84+
(root / "submission.json").write_text(json.dumps(submission, sort_keys=True) + "\n")
85+
86+
87+
if __name__ == "__main__":
88+
main()
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#!/bin/sh
2+
set -eu
3+
python /solution/solve.py

0 commit comments

Comments
 (0)