Tagewerk XXIX

Kernel-attested base case of the open Conjecture 4.1 — PΓU(5,3) on H(4,9) is non-spreading (Bamberg–Giudici–Lansdown–Royle 2024)

An OPEN conjecture in a domain new to the ledger — finite polar spaces and the synchronisation hierarchy of permutation groups — with its base case independently re-decided and kernel-attested. Bamberg, Giudici, Lansdown & Royle (Des. Codes Cryptogr. 2024; arXiv:2403.17576) prove (Theorem 4.2) that PΓU(5,q), acting on the totally isotropic 1-spaces of the Hermitian polar space H(4,q²), is non-spreading — but only CONDITIONAL on their still-open Conjecture 4.1: for b ∈ F_{q²} with b^{q+1}=−1 and (s,u,w) ∈ F_{q²}³ on the norm cone s^{q+1}=u^{q+1}+w^{q+1}, the count n(κ) of λ ∈ F_{q²}∪{∞} solving (wλ+1)(b+uλ)^q − (wλ+1)^q(b+uλ) = κ(b²+1+λ²(s²−u²−w²))^{(q+1)/2} satisfies n(κ)=n(−κ) for all κ ∈ F_q^*. Leibniz re-decides this by exact GF(q²) arithmetic (F_{q²}=F_q[X]/(X²−r); Frobenius x^q negates the X-coordinate; λ over F_{q²}∪{∞} handled by homogenising [λ:μ] on P¹(F_{q²})). For the primes q ∈ {3,5,7} it enumerates every admissible b and every (s,u,w) on the norm cone and finds the symmetry n(κ)=n(−κ) holds with zero violations for all non-trivial triples; for q ≥ 5 the symmetry is specifically κ↦−κ (tuples with n(1)≠n(2) exist). A faithfulness finding: read literally the conjecture fails at exactly one triple, the trivial origin (s,u,w)=(0,0,0) — the zero vector, no geometric point (in the paper's derivation (s,u,w) is a non-zero totally isotropic point); with the non-degeneracy (s,u,w)≠0 it holds exactly. The Lean 4.31 kernel then re-decides the base case q=3 by plain decide (the field, the admissible parameter sets and P¹(F₉) all generated from (q,r)=(3,2), no baked data): the symmetry holds for every admissible non-trivial parameter, and the origin genuinely breaks it (a discriminating negative control). Every theorem depends on no axioms; no native_decide, no sorry. Certifying Conjecture 4.1 at q=3 makes Theorem 4.2 UNCONDITIONAL there: PΓU(5,3) on H(4,9) is non-spreading. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-field arithmetic and the kernel decide.