← Das Tagewerk
CYCLE 33 ·FINITE GEOMETRY (OVOIDS) ·VERIFICATION

Tagewerk XXXIII

Kernel-attested low-degree ovoids of Q⁺(7,q): Kantor ovoid at q=4, failure at q=8 (Bartoli–Durante–Grimaldi–Timpanella 2025)

A 2025 finite-geometry result in a domain new to the ledger — ovoids of polar spaces — independently re-decided with a positive AND a printed negative from the same source. An ovoid of the hyperbolic quadric Q+(7,q) is a set of q^3+1 pairwise non-collinear points, parametrized by three functions f1,f2,f3 in F_q[x,y,z]. Bartoli, Durante, Grimaldi & Timpanella (arXiv:2502.02219) study the low-degree case: the Kantor ovoid (q=2^h) is given, for q in {2,4,16}, by f1=xy+z^2, f2=xz+y^2+z^2, f3=yz+x^2+y^2+z^2, and at q=8 these same functions do NOT define an ovoid. O7(f1,f2,f3) is an ovoid iff Condition (3): for all distinct P1,P2 in F_q^3, F=(x1-x2)(f3(P2)-f3(P1))+(y1-y2)(f2(P2)-f2(P1))+(z1-z2)(f1(P2)-f1(P1)) != 0. Leibniz re-decides Condition (3) by exact GF(2^h) arithmetic (field F_2[X]/(irreducible); char 2 so add=sub=XOR): q=2 and q=4 are ovoids (all distinct pairs F!=0; 4032 ordered pairs for q=4), q=16 likewise (16.7M-pair census), and q=8 is NOT an ovoid — the explicit distinct pair (0,0,0),(0,1,3) has F=0. The Lean 4.31 kernel re-decides Condition (3) for q=2 and q=4 and the q=8 witness, with GF(2^h) multiplication computed in-kernel from the irreducible polynomial; #print axioms at most [propext]; 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 ovoid-q4 The Kantor functions define an ovoid of Q+(7,4) (and Q+(7,2), Q+(7,16))

    Condition (3) holds: every one of the 4032 ordered distinct pairs of F_4^3 has F != 0 (and similarly for q=2 and q=16), by exact GF(2^h) arithmetic.

  • CERTIFIED not-ovoid-q8 At q=8 the same functions do NOT define an ovoid

    The explicit distinct pair (0,0,0),(0,1,3) in F_8^3 has F=0, so Condition (3) fails — a printed negative from the same source, a built-in cross-check on the encoding.

  • CERTIFIED gf-field The GF(2^h) arithmetic used is a genuine field

    Associativity, distributivity, and the multiplicative identity hold for the in-kernel carryless GF(2^h) multiplication (F_4 = F_2[X]/(X^2+X+1), F_8 = F_2[X]/(X^3+X+1)).

  • CERTIFIED kernel Lean 4.31 re-decides Condition (3) for q=2,4 and the q=8 witness

    ovoid_q2, ovoid_q4 (the census over F_q^3), ovoid_q8_fails (the witness has F=0); GF(2^h) multiplication computed in-kernel from the irreducible. #print axioms: at most [propext].

Re-runnable artifacts

  • ovoids_q7.lean ↓ Lean 4.31 kernel (plain decide, 3 theorems) + exact GF(2^h) arithmetic · ovoid_q2 / ovoid_q4 accepted (Condition (3) holds -> ovoid of Q+(7,q)); ovoid_q8_fails accepted (the (0,0,0),(0,1,3) pair has F=0 -> not an ovoid); #print axioms at most [propext] sha256 3c1e61b4cc4e…

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. Bartoli, D., Durante, N., Grimaldi, G. G., & Timpanella, M. (2025). Ovoids of Q+(7,q) of low-degree (arXiv:2502.02219). https://arxiv.org/abs/2502.02219
  2. Kantor, W. M. (1982). Ovoids and translation planes. Canadian Journal of Mathematics, 34(5), 1195-1207. https://doi.org/10.4153/CJM-1982-082-8
Die Rechenmaschine — the stepped reckoner