The Frobenius number of a shifted square sequence: a complete formula, the genus, and a sharp bound at a ≡ 7 (mod 8)
Abstract
For an integer a ≥ 2 let Sₐ be the numerical semigroup generated by the shifted squares a, a+1², a+2², a+3²,…, and let F(a) be its Frobenius number. Liu and Xin determined F(a) under a hypothesis — the existence of an r<a with ι(r)=4, ι(a+r) ≥ 3, ι(2a+r) ≥ 2, where ι(n) is the least number of positive squares summing to n — and conjectured that the hypothesis holds for every a>30; their table records three values of a that neither of their two theorems reaches. We give a formula for F(a) that is valid for every a ≥ 2 with no hypothesis and no case left over: writing n=ta+r with 0 ≤ r<a, membership in Sₐ is decided by at most four evaluations of ι, the gap set lies in [0,4a), and F(a) is read off the highest non-empty of four rungs, the top two of which are the theorems of Liu and Xin. The same description gives the genus |ℕsetminusSₐ| as an explicit count of at most 4a points, a quantity neither source computes. We also prove F(a) ≥ 4a-8 for a ≡ 7 (mod 8), a ≥ 15, sharpening the constant 48 of Song for that class by a factor of six, with equality already at a=15; and we prove Liu and Xin's Theorem 2.8 and their Conjecture 2.10, the latter by a single congruence class rather than a case analysis, which in particular covers a=73 and a=77. All statements are machine-checked in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
91dea70987762988723467793e6f228e42515c0f66905d2586f5da7094992b17
Claim ledger
Stated results
frobsq-01routine2026-08-22
The Apery/Bellman certificate determines F(S(A(a))), with a proved cap: any K with 4a <= K² suffices
frobsq-02known data2026-08-22
F(S(A(a))) for a = 2..80, by kernel decide (no native_decide axiom)
frobsq-03routine2026-08-22
F(S(A(a))) for a = 81..250, by native_decide
frobsq-04routine2026-08-22
iota(n), the least number of positive squares summing to n, is decidable and iotaB computes it
frobsq-05known2026-08-22
Liu-Xin's formula 3a + maxr equals the certified Frobenius number, at 235 values of a
frobsq-06known data2026-08-22
The conjecture's hypothesis set is empty at exactly 15 values of a <= 250, all at most 30
frobsq-07routine2026-08-22
Negative controls: F is exact, the cap hypothesis is load-bearing, neither Bool half is vacuous, a >= 2 is needed
frobsq-08known2026-08-28
n ∈ S(A(a)) ↔ ∃ j, j·a ≤ n ∧ ι(n−j·a) ≤ j — the membership criterion, proved from the definition by closure induction plus zero-padding
frobsq-09known2026-08-28
[Liu–Xin] Theorem 2.8 proved as a theorem, not instantiated 235 times
frobsq-10candidate2026-08-28
The complete unconditional formula: IsFrobenius (semi a) (frobLadder a) for every a ≥ 2, four rungs, no hypothesis
frobsq-11known2026-08-28
[Liu–Xin] Conjecture 2.10 proved: for every a ≥ 31 the hypothesis set of Theorem 2.8 is non-empty
frobsq-12known2026-08-28
Closed forms: F(S(A(a))) = 4a − 1 for 8 ∣ a, and 4a − 5 ≤ F ≤ 4a − 1 for a ≡ 4 (mod 8) (a >= 8 resp. a >= 12)
frobsq-13candidate2026-08-28
The genus: |ℕ S(A(a))| = genusB a, an explicit count of at most 4a points
frobsq-14routine2026-08-28
Negative controls for the ladder/conjecture layer
frobsq-15candidate2026-08-28
a ≡ 7 (mod 8), a ≥ 15 ⟹ F(S(A(a))) ≥ 4a − 8
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Sources.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7