# AI provenance: The Welch function is not third-order sum-free

Author: Deep Bhattacharjee (sole author). No AI system is an author or contributor.

## How the work was produced

Deep Bhattacharjee chose the problem, Conjecture 4.10 of Hou and Zhao (arXiv:2609.31489), and directed the work. Claude (Anthropic), through Claude Code, searched the literature, found and checked the proofs, wrote the verification programs in C, C++, Bash, Python, Julia and Lean 4, wrote the Lean 4 proofs with Mathlib, and drafted the paper.

## How the results are checked

The proofs are complete by hand in the paper. In addition:

- `verification/c/welch_criterion.c`: every x in F_(2^n) for odd 3 ≤ n ≤ 21: dim Z(x) ∈ {2,3} by Gaussian elimination, Theorem 1.1 at every x, Theorem 1.2 with K_n summed directly.
- `verification/cpp/welch_subspaces.cpp`: the zero-sum three-dimensional subspaces counted from the definition for n = 3, 5, 7, 9, 11 (1, 0, 127, 1606, 22517).
- `verification/python/verify_steps.py`: the polynomial identities of Section 3 and every lemma of Sections 3 and 4 at every x for n ≤ 13.
- `verification/julia`, `verification/shell`: Theorem 1.2 for odd n ≤ 23, positivity for odd 7 ≤ n ≤ 61, and Table 1.
- `verification/lean/`: a kernel certificate for n = 5 and n = 7, and Lean 4 with Mathlib for the algebraic identities, with the standard axioms only.

## What is claimed

Conjecture 4.10 of Hou and Zhao in full: for every n = 2m+1 ≥ 7 the Welch function X^(2^m+3) on F_(2^n) sums to zero over some three-dimensional affine subspace, and it does so over exactly (2^n+1−3K_n)(2^n−1)/168 three-dimensional linear subspaces.

## Labels given on the Hexagon form

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

## Where everything is

Release v1.1.0: https://github.com/creelie/eConjectureWelchSumFree/releases/tag/v1.1.0