# AI-use and process summary

*Low-discrepancy quasi-uniform digital nets in every dimension*, version 1 — Leonhard Gruenschloss. Supplementary disclosure (ancillary file; it is not part of the paper).

## Statement

The constructions, proofs and Lean formalization were produced by AI systems (Anthropic Claude Opus 5.5; some early exploratory results used Claude Fable 5.1) under the author's direction. The author selected the problems, steered the research and reviewed the formal statements, but has not verified every proof by hand. AI systems are not listed as authors; responsibility for the deposit rests with the author.

## Systems used

- **Anthropic Claude**, run as agentic sessions in Claude Code: one coordinating session per working day, which
  delegated work to sub-agents (parallel sessions of the same model family with their own tools: shell, compilers,
  Python, Lean). Model versions: Claude Opus 5.5 (`claude-opus-5-5`) for the main work (constructions, proofs,
  manuscript, Lean formalization, deposit preparation); some early exploratory results used Claude Fable 5.1.
- **Tools run by the agents:** C++ (g++) and Python (uv; numpy, sympy, mpmath) for searches, exact certificates and
  independent re-implementations; Lean 4 (`v4.35.0-rc3`) with Mathlib; Comparator with the Lean kernel and NanoDa;
  occasional cloud batch jobs (Google Cloud) for larger searches, launched only after the author approved a written
  cost estimate.

## What the AI systems did

- Explored constructions (finite searches, small-case enumeration), proposed conjectures and proved them; wrote every
  proof in the manuscript.
- Wrote the C++/Python programs and the exact certificates cited in the appendix on computations, including
  independent second implementations by separate agents.
- Drafted the manuscript and all of its revisions (first draft 2026-09-27; version 1 on 2026-10-13), and ran
  adversarial review rounds: separate agents tried to refute statements, recomputed every printed number (every
  printed bound is checked to be a valid truncation), checked label references and statement-versus-proof
  consistency, and acted as referees of whole revisions (the audit and referee reports are kept in the author's
  research repository, which is not public).
- Drafted the Lean statements from the manuscript, developed all Lean proofs (one statement library of 616 compared
  theorems, and Theorem A as a separate Palomar entry), wrote fidelity checks against the manuscript's examples and
  independent generators, and ran Comparator.
- Built the interactive explainers (https://lgruen.github.io/separated-nets-lean/explainers/), whose computations are cross-checked against the paper's
  scripts.

## What the author did

- Chose the problems and the research direction (well-separated digital nets, the question of Dick, Goda and Suzuki;
  the decision to aim for explicit constructions rather than searches; scope decisions such as restricting to t = 0
  and formalizing everything the paper proves).
- Steered the work day by day: redirected unproductive routes, required that negative results be stated as evidence
  rather than as impossibility unless proved, required independent verification of claims before they entered the
  paper, and approved compute spending.
- Selected the results that form the paper, and reviewed the formal statements: the statement of Theorem A (the
  Palomar entry) was reviewed against the manuscript and signed off on 2026-10-12. The statements of the other
  library theorems the author accepts on the basis of statement-review notes prepared in AI-assisted review passes
  (each formal statement in words next to the printed statement, with every divergence); recorded 2026-10-13.
- Has read parts of the manuscript but has not verified every proof by hand; human understanding is therefore declared
  as "some".

## Time span

The broader project (three-dimensional nets with large minimum distance) ran from June 2026. The line of work of this
paper ran from 2026-09-26 to 2026-10-13 (about 640 commits to its directory of the research repository); the Lean
formalization was carried out from 2026-10-07 to 2026-10-12, and its final Comparator run (all 616 theorems, both
kernels) completed on 2026-10-13.

## Routes that did not work (summary)

Proved obstructions (written out in the research notes): subgroups of (Z/b^m)^3 are never (0,m,3)-nets for m ≥ 2;
integer-linear ("chain-ring") rules with carries do not give nets for n ≥ 2; exact rods of points along (1,1,1) are
impossible; a periodic top-digit pattern is exactly a truncated net, so the "pattern plus completion" idea moves all
difficulty into the completion; spatial doublings of nets are copy-lifts and carry no seed geometry. Abandoned on
evidence only (finite searches, not proofs): symmetric nets (10–15 % below the best searched nets), prototile
substitution, nonlinear (non-digital) variants of the lifts (no gain over digital in the cases tried), and
higher-order eigenbasis closed forms (which reached only moderate separation). The review rounds and the
formalization also caught statements that claimed more than their proofs gave; such statements were corrected or
removed in the next revision.

## Verification layers

1. Lean 4 + Mathlib: all 616 statements of the library are proved and accepted by Comparator with the Lean kernel and
   NanoDa; Theorem A is also a separate Palomar entry (PALOMAR-2026-10-13-000011, version 1). As the paper states (appendix on formal
   verification), every theorem, proposition, lemma and corollary is formalized, apart from finite computations whose
   printed values no formalized result needs (checked by scripts); two classical theorems not in Mathlib enter as
   explicit hypotheses (the prime number theorem for the growth constant of the design U_s; Hajós's theorem, Keller's
   property for s ≤ 7 and the optimal packing bounds in dimensions two and three for the cube proposition).
2. Programs that recompute every computed value and regenerate every figure printed in the paper, with a driver that
   fails on any disagreement (https://github.com/lgruen/separated-nets-lean, directory `paper/scripts/`; Zenodo doi:10.5281/zenodo.23327748).
3. Partial human reading by the author.

## Links

- Repository (Lean formalization, LaTeX source, scripts): https://github.com/lgruen/separated-nets-lean (release v1.0.0 = version 1)
- Zenodo archive: https://doi.org/10.5281/zenodo.23327748 (concept DOI, all versions); release v1.0.0:
  https://doi.org/10.5281/zenodo.23327749
- Lean blueprint: https://lgruen.github.io/separated-nets-lean/blueprint/
- Interactive explainers: https://lgruen.github.io/separated-nets-lean/explainers/
- Palomar entry (Theorem A), PALOMAR-2026-10-13-000011 version 1: https://palomar-registry.org/entry?id=PALOMAR-2026-10-13-000011&version=1