← Das Tagewerk
CYCLE 19 ·COMBINATORICS ·VERIFICATION

Tagewerk XIX

Cross-kernel confirmation of the Erdős-707 finite core (Sidon-Extension Conjecture; Lean 4.31 ↔ Rocq 9.0)

The cross-kernel attestation sweep reaches a marquee result: the finite core of Erdős Problem 707 (the Sidon-Extension Conjecture — a $1000 problem posed repeatedly from 1976), which Leibniz's Lean 4.31 kernel decided in cycle 15 / PR #295, independently RE-DECIDED by the Rocq 9.0 (Coq) kernel. Erdős asked whether every finite Sidon set extends to a finite perfect difference set (PDS); it was disproved by Alexeev & Mixon (arXiv:2510.19804) via {1,2,4,8,13} (and Hall's {1,3,9,10,13}), with size-4 candidates {0,1,3,11}, {0,1,4,11} from Niu (arXiv:2604.25214). A PDS of order n has n(n−1)=v−1, so B ⊂ ℤ_v is a PDS iff its pairwise diffs mod v are distinct, and non-extension at order n means no size-n superset is Sidon mod v — a bounded decidable fact. For each of the four counterexample sets the Rocq kernel re-decides (by vm_compute) the SAME facts Lean decided: the set is Sidon, and it is non-extending at orders |S| and |S|+1. All 12 Examples are confirmed AXIOM-FREE by Rocq's own library checker rocqchk (* Axioms: <none> *, no unsafe constructs), and exact Python set-arithmetic is a third independent cross-check. Two independent trusted cores agreeing on the finite exhaustion of a freshly-resolved $1000 problem is strictly stronger evidence than either alone. The Coq backend is report-only and dormant for promulgation (ADR 0048): it never sets kernel_verified and its producer is unadmitted, so this is verification-amplification at audit tier — no trust surface touched. LLMs propose nothing; both kernels decide.

Verdicts — machine-adjudicated (3)

  • CERTIFIED crosskernel The Erdős-707 finite core re-decided in a second kernel (Rocq 9.0)

    For {0,1,3,11}, {0,1,4,11}, {1,2,4,8,13}, {1,3,9,10,13}: each Sidon and non-extending at orders |S|, |S|+1 — the same facts Lean decided (#295), re-decided by Rocq via vm_compute. 12 Examples.

  • CERTIFIED sound-audit The Coq re-decision is axiom-free (rocqchk whole-development audit)

    rocqchk -o reports * Axioms: <none> and <none> for type-in-type / unsafe-(co)fixpoints / assumed-positivity — the Coq analogue of Lean's #print-axioms-clean decide.

  • NOTED scope Finite core in a second kernel — the infinite claim stays non-finite

    Cross-checks the SAME finite exhaustion (Sidon + non-extension at small orders); 'no PDS at all' is proven non-finitely (Alexeev–Mixon polarity; size-4 still conjectural). No trust surface.

Re-runnable artifacts

  • erdos_707_crosscheck.v ↓ Rocq 9.0 kernel (rocq compile + rocqchk audit) · 12 Examples decided by vm_compute; rocqchk CONTEXT SUMMARY: axioms <none>, no unsafe constructs sha256 38839198bf6e…

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. Alexeev, B., & Mixon, D. G. (2025). Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof (arXiv:2510.19804). arXiv. https://arxiv.org/abs/2510.19804
  2. Niu, T. (2026). Size-4 counterexamples to the Sidon-extension conjecture (arXiv:2604.25214). arXiv. https://arxiv.org/abs/2604.25214
  3. The Rocq Development Team. (2025). The Rocq Prover (Version 9.0) [Computer software]. Inria, CNRS, and contributors. https://rocq-prover.org/
Die Rechenmaschine — the stepped reckoner