How far a conic of PG(2,q) extends to an (n,3)-arc: the exact maximum for q=3,5,7,11,13,17,19
Abstract
Let O be a conic of PG(2,q), q odd, and let m(q) be the largest m for which some m points off O can be added to it so that the union is a (q+1+m,3)-arc, i.e. meets every line in at most three points. Dönmez, Akpinar and Pelen (arXiv:2608.18192) ask for m(q) as a function of q; they prove m(q) ≥ 5 for every odd prime power q and m(q) ≥ 6 for every odd prime power q ≥ 11, and report from the literature that m(7)=m(9)=7 and from a randomized search that m(13) ≥ 8. We determine m(3)=5,quad m(5)=5,quad m(7)=7,quad m(11)=7,quad m(13)=8,quad m(17)=9,quad m(19)=10. Each value is a pair of machine-checked statements: an explicit witness set, verified by evaluating the arc condition inside the Lean 4 kernel, and an upper bound obtained from one exhaustive depth-first packing search over the q² points off the conic (257 437, 1 105 078, 18 657 443 and 55 313 459 search nodes at q=11,13,17,19), whose completeness is a proved lemma and whose run is a single compiled evaluation; no certificate is stored. Outside the formal development the same search gives m(9)=7 and m(23)=11. Consequences: q=11 is the first odd q at which a conic does not extend to an (n,3)-arc of the largest size m₃(2,q) of its plane (19<21 and 22<23); the five-point construction of the source is of maximum size exactly at q=3,5 and its six-point construction at none of q=11,13,17,19; and m(q)/q decreases from 1.00 at q=7 to 0.48 at q=23, so that m(q)=⌊ (q+1)/2⌋, which fits q=17,19, fails at q=23. No growth law is claimed.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
c2d3286443a4b4bfe5a203178f97f0c18d178ea16166bfdb68ff86a5f2f595ea
Claim ledger
Stated results
CA1routine2026-09-07
The conic of PG(2,3) extends by at most m(3) = 5 points to a (9,3)-arc, and does so
CA2routine2026-09-07
The conic of PG(2,5) extends by at most m(5) = 5 points to an (11,3)-arc, and does so
CA3known data2026-09-07
The conic of PG(2,7) extends by at most m(7) = 7 points to a (15,3)-arc, and does so – the reproduction of the source's own reported value
CA4candidate2026-09-07
An explicit seven-point set makes the conic of PG(2,11) a (19,3)-arc (kernel-checked, with a trisecant exhibited)
CA5candidate2026-09-07
No eight points extend the conic of PG(2,11) to a (20,3)-arc: the exhaustive search over the 121 points off the conic is empty at target 8
CA6candidate2026-09-07
m(11) = 7: the maximal number of points by which a conic of PG(2,11) extends to a (12+m,3)-arc is exactly 7
CA7known data2026-09-07
An explicit eight-point set makes the conic of PG(2,13) a (22,3)-arc – the source's randomized-search datum, kernel-certified
CA8candidate2026-09-07
No nine points extend the conic of PG(2,13) to a (23,3)-arc: the exhaustive search over the 169 points off the conic is empty at target 9
CA9candidate2026-09-07
m(13) = 8: the conic of PG(2,13) extends by exactly 8 points and no more
CA10candidate2026-09-07
An explicit nine-point set makes the conic of PG(2,17) a (27,3)-arc
CA11candidate2026-09-07
No ten points extend the conic of PG(2,17) to a (28,3)-arc: the exhaustive search over the 289 points off the conic is empty at target 10
CA12candidate2026-09-07
m(17) = 9
CA13candidate2026-09-07
An explicit ten-point set makes the conic of PG(2,19) a (30,3)-arc
CA14candidate2026-09-07
No eleven points extend the conic of PG(2,19) to a (31,3)-arc: the exhaustive search over the 361 points off the conic is empty at target 11
CA15candidate2026-09-07
m(19) = 10
CA16routine2026-09-07
Model control, q = 7, kernel-only: the coordinate lists are a projective plane of order 7 (57 distinct points, 8 per line, exactly one line through each pair), the conic is the 8 distinct points of X₁² = X₀ X₂ inside it, met by every line in at most two, and the candidate list is exactly the 49 points off the conic
CA17routine2026-09-07
The same model control at q = 11: 133 distinct points, 12 per line, exactly one line through each of the 8 778 pairs, a 12-point conic met in at most two, and 121 candidates off it
CA18routine2026-09-07
Negative control, too large: adding (1,0,2) to the seven-point witness at q = 11 is refuted by the checker, and the line (1,5,5) is exhibited carrying four points of the union
CA19routine2026-09-07
Negative control, too small: m(11) <= 6 is false
CA20routine2026-09-07
Non-vacuity: every cardinality 0..7 is realised by an extension of the conic of PG(2,11)
CA21prose2026-09-07
q = 11 is the first q at which a conic does *not* extend to a maximum-size (n,3)-arc of its plane: 19 < 21 = m₃(2,11) and 22 < 23 = m₃(2,13), whereas the conic reaches m₃(2,q) for every q <= 9
This ledger entry is reported in prose and is not bound to a Lean theorem.CA22known data2026-09-07
m(9) = 7, reproducing the source's second reported value, computed outside Lean
This ledger entry is reported in prose and is not bound to a Lean theorem.CA23measurement2026-09-07
Cost: the family's searches are 34x faster with the compiled core than in Lean's IR interpreter (q = 11: 1.68 s vs 57.4 s), and compiled Lean is 24-31x slower than the same algorithm in gcc -O2
This ledger entry is reported in prose and is not bound to a Lean theorem.CA24prose2026-09-07
m(23) = 11: the conic of PG(2,23) extends by exactly 11 points to a (35,3)-arc and by no more – computed exhaustively, not kernel-bound
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Founded 2026-09-07 from arXiv:2608.18192v1 (Sinan Donmez, Atilla Akpinar, Rumi Melih Pelen, *Near-MDS codes of lengths q+6 and q+7 from conics in PG(2,q), q odd*, 18 Aug 2026, cs.IT + math.CO), whose Problem 6.2 poses, verbatim:
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7