# AI provenance: Reflexive Descent to Minimal Seeds in the Kreuzer–Skarke List

Authors: Deep Bhattacharjee and Ushashi Bhattacharya. No AI system is an author or contributor.

## How the work was produced

Deep Bhattacharjee chose the problem, directed the work and ran the computations. Claude (Anthropic), used through Claude Code under his direction, produced the proofs, the Lean 4 file, the programs, the figures and the LaTeX text, which the authors reviewed. The search for long descents and for the certificate of depth 22 was organised on the BLLM engine Anaxia (eBLLM release 3.0.5, https://github.com/creelie/eBLLM/releases/tag/v3.0.5), rerun on release 3.1.1 and kept in release 3.2.1. The bound in every dimension follows by hand from Blichfeldt's theorem and the volume bound of Balletti, Kasprzyk and Nill. The Kreuzer-Skarke list is due to Kreuzer and Skarke and is read from its public copy. Both authors approved the final version.

## How the results are checked

The theorems are proved in the paper from finite data computed from the Kreuzer-Skarke list, which is archived. The certificate of depth 22 (5,592 polytopes with their complete lists of covers) and the descent of the 680-point polytope are rechecked by independent programs (87 checks, 98 with the full run). 27 Lean 4 theorems, each axiom-free or depending on propext only.

## What is not claimed

The exact value of D_4 is not determined: the paper proves 22 <= D_4 <= 348.

## Labels given on the Hexagon form

- Text of the contribution: a mix of human-written and AI-generated (to be confirmed by the authors).
- Human understanding at submission: some parts, but not all, checked and understood by a human (to be confirmed by the authors).

## Where everything is

Release v1.2.0: https://github.com/creelie/seed/releases/tag/v1.2.0.