← Das Tagewerk
CYCLE 28 ·FINITE GEOMETRY ·VERIFICATION

Tagewerk XXVIII

Kernel-attested minimal double blocking sets of size 3q−1 in PG(2,q), refuting a 1984 Hill conjecture (Csajbók–Héger 2019)

A published finite-geometry result in a domain new to the ledger — blocking sets in projective planes — independently re-decided and kernel-attested. A double blocking set of PG(2,q) is a set of points meeting every line in at least two points; it is minimal if no proper subset does. The trivial one (three sides of a triangle) has size 3q, and Ball–Blokhuis (1996) proved 3q is the minimum for q ≤ 8. Csajbók & Héger (European J. Combin. 78 (2019), 655–678; arXiv:1805.01267) refute R. Hill's cautiously-stated 1984 expectation that no size-(3q−1) double blocking set with two (q−1)-secants exists: by a MIP search they exhibit explicit minimal double blocking sets of size 3q−1 admitting two (q−1)-secants for q ∈ {13,16,19,25,27,31,37,43}, the first sets of size below 3q for prime q > 13. Together with their Section-3 non-existence theorem this resolves two 1984 Hill conjectures. Leibniz amplifies the constructive half (existence). From the points printed in the paper, over the five PRIME cases q ∈ {13,19,31,37,43} (finite field ℤ/qℤ), it reconstructs each set B — both coordinate axes minus four holes, plus the printed points — and verifies by exact GF(q) incidence arithmetic, two independent ways: (1) DOUBLE BLOCKING — every one of the q²+q+1 lines meets B in at least two points (no 0- or 1-secant); (2) MINIMALITY — every point of B lies on a 2-secant, so deleting it leaves a 1-secant. As a faithfulness anchor it reproduces the paper's published secant distribution nₜ (t ≥ 3) exactly in every case (a single mis-transcribed point would shift it), with the two nₜ=2 long secants being exactly the two (q−1)-secants Hill's conjecture forbade. The Lean 4.31 kernel then re-decides both properties, plus a discriminating negative control (B minus one point is NOT double blocking), for the flagships q = 13 (the unique example with two (q−1)-secants up to equivalence) and q = 19 (the first prime q > 13), by plain decide — every theorem depends on no axioms; no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-field arithmetic and the kernel decide.

Verdicts — machine-adjudicated (4)

  • CERTIFIED exists-3q-1 Minimal double blocking sets of size 3q−1 exist in PG(2,q) for prime q ∈ {13,19,31,37,43} — smaller than the trivial 3q triangle

    Reconstructed from the paper's points; each has |B| = 3q−1 (38, 56, 92, 110, 128) and every one of the q²+q+1 lines meets it in ≥ 2 points, verified by exact GF(q) incidence arithmetic.

  • CERTIFIED minimal Each set is minimal: every point lies on a 2-secant

    For every point p of B there is a bisecant (a line meeting B in exactly two points) through p, so B∖{p} has a 1-secant and is not double blocking. Verified exactly for all five prime cases.

  • CERTIFIED refutes-hill The two (q−1)-secants coexist — refuting Hill's 1984 conjecture

    The published secant distribution nₜ (t ≥ 3) is reproduced exactly in every case; its two n_{q−1}=2 long secants are the two (q−1)-secants Hill (1984) expected could not both occur.

  • CERTIFIED kernel Lean 4.31 re-decides blocking + minimality + a negative control for q = 13, 19

    Six plain-decide theorems (db{13,19}_{blocking,minimal,control}); the controls prove a point-deleted set is NOT double blocking (= false). #print axioms: every theorem depends on no axioms — no native_decide, no sorry.

Re-runnable artifacts

  • double_blocking.lean ↓ Lean 4.31 kernel (plain decide, 6 theorems) + exact GF(q) incidence arithmetic · db13/db19 blocking + minimal accepted, controls reject (= false); #print axioms = no axioms for all six theorems sha256 cc74ffebe362…

Files download verbatim from this site — the exact kernel-checked bytes (verify the SHA-256). See how to re-verify.

Repositories — the code trail

References

  1. Csajbók, B., & Héger, T. (2019). Double blocking sets of size 3q−1 in PG(2,q). European Journal of Combinatorics, 78, 655–678 (arXiv:1805.01267). https://arxiv.org/abs/1805.01267
  2. Ball, S., & Blokhuis, A. (1996). On the size of a double blocking set in PG(2,q). Finite Fields and Their Applications, 2(2), 125–137. https://doi.org/10.1006/ffta.1996.0009
  3. Hill, R. (1984). Some problems concerning (k,n)-arcs in finite projective planes. Rendiconti del Seminario Matematico di Brescia, 7, 367–383.
10001 20010 40100 81000
De Progressione Dyadica — the binary table, 1679