Kentaro Amauchi

Independent researcher — number theory, combinatorics, formal verification

Research interests

Let A be a finite set of odd positive integers and r_A(n) the number of subsets of A summing to n. I study a weighted count of representations by the truncations of A — obtained by deleting the elements below a threshold and shifting the target — and its ratio to r_A(n). That ratio converges, for every target, to a rational number read off A by counting alone: Γ(A) = 1 + 2∑_d2^−N_A(d), where N_A(d) is the number of elements of A that are at most 2d. For the odd primes Γ = 5.3492879…, and the twin pairs are what make it small.

The counted quantity has a second reading, which is where the question came from: it counts the strict local minima of the subset-sum landscape of A. A reader who wants none of that may take the displayed identity as the definition; nothing is lost.

A recurring theme is replacing heuristic independence assumptions — the “annealed approximation” of statistical mechanics — with exact identities plus hypotheses that can actually be checked. The identity that does most of that work is a classical one, the Kubert distribution relation; the contribution is what it is made to replace.

The structural results are formally verified in Lean 4 with Mathlib — no sorry, no axiom beyond Lean's standard three, and an independent kernel replay on top of the build. The analytic parts are not formalised, and I would rather say so here than let the sentence above be read as covering them. Every statement in every paper instead carries an explicit status at the statement: proved in Lean, proved, derived, experimentally confirmed with the range given, or conjecture. The descriptions below use the same vocabulary, and are meant to be the least flattering true description of each paper.

Papers

Three parts, in preparation for arXiv (math.NT), and one standalone note. An earlier draft circulated in four instalments; the third has since been absorbed into Part III and no longer exists as a separate document.

Arithmetic landscapes I: the gap seriescomplete

Introduces Γ; proves the convergence above, a classification theorem for the strict local minima of subset-sum landscapes, a window identity W_D(A) = Γ(A) + (2D+1)/2^k, an exact stratification reducing the ratio to the flatness of representation counts of truncations, and sharp extremal bounds 3 − 2^{1−(M−1)/2} ≤ Γ(A) ≤ M with both equality cases. Its structural part is verified in Lean 4.

Arithmetic landscapes II: asymptotic flatness of subset-sum landscapes of primescomplete

The analytic half: the complete sub-peak spectrum of the characteristic product, modulus 6 as the unique maximiser, and hence lm/r → Γ(P) = 5.3492879… for the odd primes at a geometric rate. The theorem carries no hypothesis. One constant is ineffective, via Siegel–Walfisz, and the statement says which.

Arithmetic landscapes III: deformed measures, random sequences, and the coset identitymixed by section

Opens with an exact identity for X(t) = −log|cos πt|: averaging X over a coset of index v returns the same function at v times the frequency, plus a constant. The identity is classical — the Kubert distribution relation for log|2 sin πt|, shifted — and no part of it is claimed here. What is new is the use: because X ≥ 0 the rational points are the minima of the coset average, which removes the quantitative equidistribution input a minor-arc argument would normally need. Then the Bernoulli(q) deformation Γ^(q), a modulus-4 theorem, the minor-arc rate 1/√2 for random odd sequences, and the behaviour of the ratio away from the centre through an explicit transfer function. Three of its theorems were conditional on one named open problem; that problem was closed, and since v1.1.0 the three are unconditional. The rest are proved, Lean-verified, or experimentally confirmed with the range given, item by item.

Two speeds at the boundary: zeros of sums of conjugate sections of power seriesstandalone note

Twelve pages, with no prerequisites from the papers above and no citations to them — deliberately, so that a reader need not decide whether to trust the rest before deciding whether the question is interesting. On the symmetry line the object is real, so its zeros are sign changes. Two theorems are proved: the first zero satisfies t₁ > ½tan(π/k) for every non-increasing weight profile, and for weights (j+1)^−s with s > 1 the rate is exactly 2kt₁²/log k → s − ½. Below s = 1 — where the weights stop being summable — the answer changes shape, and there it is measured rather than proved; the note says which is which at each statement, and the written proof of the second theorem is in the repository beside it.

Software

arithmetic-landscapes — the three papers and the note, the Lean 4 development, and every numerical experiment together with its log. Archived at doi:10.5281/zenodo.21941261 — which makes a version permanent, not true. The Lean development carries no sorry and no axiom beyond Lean's standard three, and is replayed independently through the kernel with a negative control. A number with no log is treated as a number that does not exist, and the repository's own checks enforce that — along with the rule that every theorem, proposition, lemma and corollary must declare its status at the statement.

Use of AI tools

This work was carried out with substantial assistance from large language models (Anthropic's Claude), used for exploring constructions, drafting and checking proofs, writing the Lean formalisation, and running and analysing the numerical experiments. I direct the research, decide what is claimed, and am responsible for every statement. The verification apparatus described above exists because of this: the Lean development, the kernel replay, the logged experiments and the repository's mechanical checks are how a claim earns its status rather than being asserted. The same disclosure appears in each paper.

Contact

amkn.sub03@gmail.com