For a finite set A ⊂ ℕ we
write
A + A = {a + b : a, b ∈ A}, AA = {ab : a, b ∈ A},
and we consider the pair (|A + A|,|AA|)
as a coarse measure of the additive and multiplicative structure present
in A. For each n ≥ 1 we define the
SPP(n) = {(|A + A|,|AA|) : A ⊂ ℕ, |A| = n}.
The guiding problem is to determine SPP(n) exactly for small n, and in particular to decide, for
each admissible integer pair (i, j), whether there
exists a set A of size n with |A + A| = i and
|AA| = j.
A first observation is that (|A + A|,|AA|)
necessarily lies in a fixed square depending only on n. Indeed, both A + A and AA are formed from the
upper-triangular table of pairs (i, j) with 1 ≤ i ≤ j ≤ n,
hence |A + A| ≤ n(n + 1)/2
and |AA| ≤ n(n + 1)/2.
On the other hand, with A = {a1 < ⋯ < an}
we have
a1 + a1 < a1 + a2 < ⋯ < a1 + an < a2 + an < ⋯ < an + an,
so |A + A| ≥ 2n − 1,
and similarly |AA| ≥ 2n − 1.
Thus SPP(n) ⊂ [2n − 1, n(n + 1)/2]2 ∩ ℤ2.
In the case of interest n = 7,
this reduces membership questions to the finite grid [13, 28]2 ∩ ℤ2.
For n ≤ 6, the profile SPP(n) has been determined by a combination of structured constructions, ad hoc pruning, and bounded computation. In these cases the search space is small enough that one can largely work directly with integer sets, aided by standard reductions (normalizations by translation and scaling, gcd conditions, and elementary constraints coming from convexity and monotonicity in the addition and multiplication tables). At n = 7, however, this approach encounters a genuine obstruction: there remain candidate pairs (i, j) whose status cannot be settled by the previously effective arguments, and whose resolution requires a more systematic method for certifying both existence and nonexistence.
Our goal is to provide an unconditional, independently checkable
determination of SPP(7) within the full
admissible square. The output we seek is not merely a list of realizable
pairs, but a proof object for each decision. Concretely, for each
realizable (i, j) we
produce an explicit witness A ⊂ ℕ with |A| = 7, |A + A| = i, and
|AA| = j,
and for each unrealizable (i, j) we produce a
certificate that can be verified without re-running the original search.
In particular, this framework resolves the four previously undecided
pairs
(21, 18), (18, 20), (18, 21), (19, 20),
by either exhibiting witnesses or providing nonexistence certificates,
thereby eliminating the last ambiguity in the n = 7 profile.
The key methodological point is that, for n = 7, brute-force enumeration over ℕ is not the correct primitive. The difficulty is not the size of the square [13, 28]2, but the number-theoretic variability of the sets A that could realize a fixed collision pattern in A + A and AA. Even if |A + A| and |AA| are specified, the magnitudes of the ai may range over many orders, and purely combinatorial constraints do not immediately translate into effective bounds on a7. This motivates the separation of the and parts of the problem.
We implement this separation by encoding the collision structure of the addition and multiplication tables as . Informally, an addition type records, for each pair (i, j) with 1 ≤ i ≤ j ≤ 7, which sums ai + aj are equal and how the distinct sums are ordered, subject to the monotonicity constraints forced by a1 < ⋯ < a7. A multiplication type is defined analogously for products aiaj. A type determines |A + A| (respectively |AA|) as the number of equivalence classes in the corresponding partition of the index set I7 = {(i, j) : 1 ≤ i ≤ j ≤ 7}. Thus, for a fixed (i, j), there are only finitely many candidate type pairs (τ+, τ×) that could yield (|A + A|,|AA|) = (i, j), and these can be enumerated up to the natural symmetries of the table.
Given a candidate pair (τ+, τ×), we translate it into a : a conjunction of explicit equalities and inequalities in variables a1, …, a7 asserting that the induced order relations among sums match τ+ and the induced order relations among products match τ×, together with the strict inequalities a1 < ⋯ < a7 and the appropriate domain constraints. Over ℝ > 0, these are quantifier-free semi-algebraic constraints of low degree. Over ℕ, they become a mixed arithmetic problem with integrality. The principal advantage is that each type pair yields a finite feasibility problem, amenable to certified real-algebraic decision procedures.
Our proof strategy proceeds in two layers. First, we work over ℝ > 0 as an auxiliary domain: since ℕ ⊂ ℝ > 0, infeasibility over ℝ > 0 immediately implies infeasibility over ℕ. This produces strong pruning and allows us to discard many candidate type pairs without any number-theoretic search. Second, for those type pairs that are feasible over ℝ > 0, we decide whether they admit rational (hence integer, after scaling) realizations or whether every realization forces an irrational parameter, in which case integrality is impossible. This is the point where certificates become essential: rather than relying on heuristic rounding or numerical recovery, we require either an explicit integer witness or an explicit solver-verifiable proof that no integer point lies in the feasible region.
The resulting outputs are organized as follows. Theorem~A gives the exact description of SPP(7) ∩ ([13, 28]2 ∩ ℤ2) as a finite set S, together with witnesses for each (i, j) ∈ S and nonexistence certificates for each (i, j) ∉ S. Corollary~B isolates the four previously unresolved pairs and records their final status. Proposition~C formalizes the role of ℝ > 0-feasibility as a pruning device and the subsequent lifting (or obstruction) step for ℕ. Proposition~D describes the reproducibility guarantees: all existence claims are accompanied by explicit sets A and recomputation checks, and all nonexistence claims are accompanied by certificates that can be validated independently (including cross-validation using more than one solver stack and a standalone verifier).
In summary, our contribution is a complete, certificate-backed classification of the n = 7 sum–product profile within the admissible square. The emphasis on types and compatibility instances converts the original existential question into a finite family of explicit decision problems, and the emphasis on certificates converts the resulting computation into a reproducible proof. The next section develops the background and motivation for these choices, beginning with the familiar extremal regimes and the structural pruning heuristics that are effective for smaller n but insufficient, by themselves, to close the n = 7 case.
We begin by recalling the extremal constructions that control the boundary of the admissible square for SPP(7), and by isolating a family of constraints—often summarized as a ``Sidon exclusion zone’’—that rules out a substantial portion of that square without any detailed search. These considerations do not by themselves settle the full n = 7 profile, but they explain why certain regions are easy and why the remaining instances require a type-based, certificate-producing approach.
At the additive extreme, the smallest possible sumset occurs when
A is an arithmetic
progression. Indeed, for A = {1, 2, 3, 4, 5, 6, 7} one
checks
A + A = {2, 3, …, 14}, |A + A| = 13 = 2n − 1,
and the general inequality |A + A| ≥ 2n − 1
is sharp in this way. At the multiplicative extreme, the smallest
possible product set is realized by a geometric progression. For
example,
A = {1, 2, 4, 8, 16, 32, 64}
satisfies
AA = {2k : 0 ≤ k ≤ 12}, |AA| = 13 = 2n − 1,
again achieving the general lower bound. These two constructions already
indicate the basic tension: additive structure (few distinct sums) is
most naturally produced by approximate additivity (an AP), whereas
multiplicative structure (few distinct products) is most naturally
produced by approximate multiplicativity (a GP). For typical sets these
tendencies are incompatible, and the profile (|A + A|,|AA|)
records the residual compatibility.
At the opposite end, the maximal value |A + A| = 28 = n(n + 1)/2
is attained when all upper-triangular sums ai + aj
are distinct; such sets are precisely (or B2) sets when expressed
in the usual language of distinct pairwise sums. Similarly, |AA| = 28 is attained when
all upper-triangular products aiaj
are distinct; we refer to such sets as sets. A convenient source of
multiplicative Sidon sets in ℕ is given
by primes: if A = {p1 < ⋯ < p7}
are distinct primes, then unique factorization implies
pipj = pkpℓ ⇒ {i, j} = {k, ℓ},
and hence |AA| = 28.
In both the additive and multiplicative settings, the point is that ``no
collisions in the table’’ corresponds to the maximal class count of the
corresponding equivalence relation on I7.
Between these extremes lie structured families that are neither close
to AP nor close to GP but still exhibit many collisions in tables. A
basic source is given by sets with many multiplicative dependencies
(e.g. divisor-closed or smooth-number patterns) together with enough
additive overlap to force sum collisions. For instance, the benchmark
set
A = {1, 2, 3, 4, 6, 8, 12}
has the feature that many elements share small prime factors, producing
repeated products, while the additive gaps are small enough to create
repeated sums as well. A direct computation gives
|A + A| = 18, |AA| = 18,
so (18, 18) ∈ SPP(7). Examples of this
kind are important for calibration: they show that moderately small
values of |A + A| and
|AA| can occur
simultaneously, but typically only when the set carries a significant
amount of arithmetic structure.
The
Sidon exclusion zone'' is the complementary phenomenon: when one table is close to collision-free, the other cannot have very many collisions. One way to formalize this is to measure how far \(A\) is from being Sidon by the defect \[ \delta_+(A)=\binom{7+1}{2}-|A+A|=28-|A+A|, \] and similarly \(\delta_\times(A)=28-|AA|\). Small \(\delta_+(A)\) means that the addition table has few equalities \(a_i+a_j=a_k+a_\ell\), which in turn forces strong constraints on the additive energy of \(A\). Over \(\mathbb{R}_{>0}\), and a fortiori over \(\mathbb{N}\), such constraints tend to prevent a large number of multiplicative collisions unless \(A\) is constrained to very special shapes. Concretely, prior work in the small-\(n\) regime establishes explicit forbidden regions in the \((|A+A|,|AA|)\)-plane: for \(n=7\), many pairs with \(|A+A|\) near \(28\) and \(|AA|\) near \(13\) are excluded by arguments that combine monotonicity in the tables with combinatorial counting of collision patterns. There is a symmetric statement with addition and multiplication interchanged, excluding pairs with \(|AA|\) near \(28\) and \(|A+A|\) near \(13\). We emphasize that these exclusions are \emph{structural}: they do not arise from bounding the magnitudes of the \(a_i\), but from the fact that a nearly Sidon pattern forces the remaining relations to behavegenerically’’.
For n ≤ 6, such structural pruning, combined with modest bounded enumeration, is often sufficient to decide membership in SPP(n). At n = 7 it remains powerful but not complete. The unresolved candidate pairs in the admissible square are not concentrated near the corners governed by AP/GP or Sidon/multiplicative Sidon behavior; rather, they occur in the intermediate regime where neither δ+ nor δ× is small enough for exclusion-zone arguments to be decisive, yet the sets realizing (or failing to realize) a given pair may require subtle collision patterns.
This intermediate regime is precisely where direct search over integer sets becomes ineffective as a proof method. Even after the standard normalizations (e.g. translating so that a1 is small, scaling by gcd (A), or fixing a1 = 1 when temporarily working over ℝ > 0), one encounters the basic difficulty that the constraints |A + A| = i and |AA| = j do not impose an a priori usable bound on a7. The same (i, j) can be realized by sets with very different magnitudes, and conversely a fixed upper bound on a7 can miss realizations whose geometry is forced by a sparse pattern of equalities in the tables. Thus, an exhaustive integer enumeration must either choose a large cutoff (which becomes computationally prohibitive) or accept incompleteness (which is incompatible with certification).
This is the point at which become natural. The data that determine |A + A| are not the values of the sums themselves but the pattern of equalities and inequalities among the 28 quantities ai + aj with (i, j) ∈ I7. Likewise, |AA| depends only on the collision pattern among the 28 products aiaj. If we separate this combinatorial information from the arithmetic realization, then the search space becomes finite: there are only finitely many weak orderings of I7 compatible with the monotonicity constraints forced by a1 < ⋯ < a7 and positivity. Each such ordering—an addition-table type τ+ and a multiplication-table type τ×—implicitly fixes the integers |A + A| and |AA| as the numbers of equivalence classes. Moreover, once (τ+, τ×) is fixed, the question of existence of A realizing it becomes a feasibility problem in explicit polynomial equalities and inequalities.
Finally, the same background considerations explain why we use ℝ > 0 as an auxiliary domain. The ordering constraints implicit in a type are expressed by strict inequalities, and the collision constraints are expressed by linear (for sums) and quadratic (for products) equations. Over ℝ > 0 this yields a semi-algebraic set that can be decided by certified real-algebraic procedures; infeasibility here is an immediate certificate of infeasibility over ℕ. When feasibility over ℝ > 0 does occur, the remaining issue is arithmetic: either one can find a rational realization (which can be scaled to an integer witness), or one can certify that every realization forces an irrational parameter and hence cannot correspond to an integer set. In this way the extremal regimes and exclusion-zone constraints motivate, but do not replace, the type-based reduction developed in the next section.
For the remainder of the argument we fix n = 7 and write A = {a1 < ⋯ < a7} ⊂ X, where X is either ℝ > 0 (for pruning and feasibility) or ℕ (for the target problem). The key point is that the values |A + A| and |AA| are determined not by the magnitudes of the ai but by the among the upper-triangular sums and products. We formalize these patterns by introducing combinatorial objects—types—whose realizability over a given domain can be decided by explicit algebraic constraints.
We index the upper-triangular entries of the addition and
multiplication tables by
I7 = {(i, j) : 1 ≤ i ≤ j ≤ 7}.
For each (i, j) ∈ I7
we associate the sum sij = ai + aj
and the product pij = aiaj.
Since a1 < ⋯ < a7
and ai > 0, these
arrays satisfy a monotonicity property along rows and columns:
sij < si + 1, j, sij < si, j + 1,
and similarly
pij < pi + 1, j, pij < pi, j + 1,
whenever the indices remain in I7. However, apart from
these forced inequalities, there may be additional equalities such as
ai + aj = ak + aℓ,
and the set of all such relations (together with the induced strict
inequalities between distinct values) is exactly what controls |A + A| and |AA|.
An τ+ is a weak ordering ≼+ on I7 satisfying the monotonicity constraints above: whenever (i, j), (i + 1, j) ∈ I7 we require (i, j)≺+(i + 1, j), and whenever (i, j), (i, j + 1) ∈ I7 we require (i, j)≺+(i, j + 1). As usual, we write (i, j)∼+(k, ℓ) if (i, j)≼+(k, ℓ) and (k, ℓ)≼+(i, j), and (i, j)≺+(k, ℓ) if (i, j)≼+(k, ℓ) but not conversely. Intuitively, (i, j)∼+(k, ℓ) encodes the intended equality ai + aj = ak + aℓ, while (i, j)≺+(k, ℓ) encodes ai + aj < ak + aℓ. The monotonicity requirements ensure that τ+ is consistent with strictly increasing positive sequence; they also guarantee that we are describing a refinement of the partial order generated by increasing either index.
The definition of a τ× is identical, replacing sums by products. Thus τ× is a weak ordering ≼× on I7 such that (i, j)≺×(i + 1, j) and (i, j)≺×(i, j + 1) whenever defined, and (i, j)∼×(k, ℓ) indicates the intended equality aiaj = akaℓ. Although the formal constraints are parallel, the arithmetic content is different: addition collisions are linear relations among the ai, whereas multiplication collisions are quadratic relations. This distinction is precisely what makes the paired analysis effective: an addition type alone describes a polyhedral region (after normalization), while a multiplication type introduces genuinely algebraic constraints.
Given a strictly increasing 7-tuple
a = (a1, …, a7) ∈ X7,
we say that a an
addition type τ+(a) by
declaring
(i, j)≼+(k, ℓ) ⇔ ai + aj ≤ ak + aℓ,
and similarly induces a multiplication type τ×(a)
via
(i, j)≼×(k, ℓ) ⇔ aiaj ≤ akaℓ.
We then define the realization sets
RealizeX(τ+) = {a ∈ X7 : a1 < ⋯ < a7, τ+(a) = τ+},
and likewise RealizeX(τ×).
When the ambient domain is clear we suppress the subscript X. A pair (τ+, τ×)
is if RealizeX(τ+) ∩ RealizeX(τ×) ≠ ∅;
equivalently, there exists a ∈ X7
inducing both types simultaneously. Our computational reduction is
organized around deciding this compatibility for finitely many candidate
pairs.
Types encode |A + A| and |AA| in the most direct way: |A + A| is the number of distinct values among the 28 sums {ai + aj : (i, j) ∈ I7}, and this is exactly the number of equivalence classes of ∼+ on I7. Likewise, |AA| is the number of ∼×-classes. Thus, if τ+ has i equivalence classes and τ× has j equivalence classes, then any common realization a yields (|A + A|,|AA|) = (i, j). Conversely, to decide whether a fixed pair (i, j) belongs to SPP(7), it suffices to consider the finite collection of type pairs whose class counts are (i, j) and test which of them admit an integer realization.
Two further features make types suitable as a proof device. First,
the search space is finite: I7 is finite, and the
monotonicity constraints restrict to weak orderings extending a fixed
partial order, so there are only finitely many admissible τ+ and τ×. Second, types support
robust normalization. Over ℝ > 0, scaling by a positive
constant c preserves both
tables up to uniform scaling:
(ai + aj) ↦ c(ai + aj), (aiaj) ↦ c2(aiaj),
so all equalities and inequalities among sums and products are
preserved. Hence, when working over ℝ > 0 we may impose the
standing normalization a1 = 1 without loss of
generality for realizability questions. In addition, translation a ↦ (a1 + t, …, a7 + t)
preserves the addition type (it adds 2t to every sum) but does not
preserve the multiplication type; this asymmetry is one reason we avoid
additive normalizations that would conflict with multiplicative
structure. Over ℕ, we similarly use
gcd (A) = 1 and the convention
of listing A in increasing
order to eliminate redundant witnesses; these normalizations do not
change the induced types, except by the obvious scaling discussed
above.
Finally, we record the symmetry considerations relevant for enumeration. Commutativity of addition and multiplication is already incorporated by restricting to I7 (upper-triangular indices), so each unordered pair {i, j} is represented exactly once. Beyond this, we do quotient by arbitrary permutations of {1, …, 7}, since the types are defined relative to the increasing order of the ai and the monotonicity constraints are expressed in these coordinates. What we do exploit is the following: if two weak orderings yield identical systems of implied comparisons after taking the monotonicity closure, we treat them as the same type; and when enumerating type pairs with fixed class counts, we identify and discard duplicates by canonical labeling of the induced ordered partition of I7. This produces a finite, explicit list of candidates for each (i, j), suitable for solver-based feasibility checks.
With these definitions in place, the reduction step is conceptually straightforward: a type τ+ specifies which linear equalities ai + aj = ak + aℓ must hold and which strict inequalities must separate distinct sum-classes; similarly τ× specifies quadratic equalities and inequalities among products. In the next stage we translate a fixed pair (τ+, τ×) into an explicit semi-algebraic feasibility instance, incorporate the chosen normalizations (such as a1 = 1 over ℝ > 0), and thereby reduce membership in SPP(7) to a finite family of certified constraint-solving problems.
Fix a candidate pair of types (τ+, τ×). Our next task is to convert (τ+, τ×) into an explicit conjunction of algebraic constraints in the variables a1, …, a7 whose solutions are precisely the common realizations of the two types (subject to the ambient domain). We refer to the resulting formula as the associated to (τ+, τ×).
We begin with the addition type τ+. Concretely, τ+ is an ordered
partition of I7
into equivalence classes
I7 = C1 ⊔ ⋯ ⊔ Ci, C1≺+C2≺+⋯≺+Ci,
where (u∼+v) if and
only if u, v lie in
the same block, and (u≺+v) if and
only if their blocks are strictly ordered. For each index u = (p, q) ∈ I7
we write su = spq = ap + aq.
The equalities prescribed by τ+ are linear: choosing a
representative rk ∈ Ck
for each block, we impose
su − srk = 0 for
every u ∈ Ck,
i.e.
(ap + aq) − (ap′ + aq′) = 0 whenever
(p, q)∼+(p′, q′).
To enforce the strict ordering of distinct sum-classes, it suffices to
impose inequalities only between blocks:
srk < srk + 1 (1 ≤ k < i).
Indeed, together with transitivity of <, this implies srk < srℓ
for all k < ℓ, and
hence separates all distinct blocks. This compression is important
computationally: the complete set of pairwise inequalities between
distinct classes can be quadratic in |I7|, whereas
adjacent-block inequalities are linear in the number of classes. We
emphasize that the choice of representatives affects only the syntactic
form of the instance; any selection yields an equivalent feasibility
problem because τ+
already fixes the relative order of the blocks.
We treat τ×
analogously. Writing pu = ppq = apaq
for u = (p, q), and
letting
I7 = D1 ⊔ ⋯ ⊔ Dj, D1≺×⋯≺×Dj
be the ordered partition into ∼×-classes, we pick
representatives tℓ ∈ Dℓ
and impose, for every u ∈ Dℓ,
pu − ptℓ = 0,
i.e.
apaq − ap′aq′ = 0 whenever
(p, q)∼×(p′, q′).
To separate distinct product-classes we again impose adjacent strict
inequalities
ptℓ < ptℓ + 1 (1 ≤ ℓ < j).
All multiplication constraints are polynomial of degree 2; this bounded degree is one reason that
CAD- and SMT-based decision procedures are effective in our setting.
In addition to the constraints encoding the two ordered partitions,
we must impose the basic ambient conditions. First, the ordering of the
underlying set is enforced by
a1 < a2 < ⋯ < a7.
Second, for the real feasibility stage we work over ℝ > 0, so we add ak > 0 for
all k. Over ℕ we replace these by integrality and
positivity constraints ak ∈ ℕ. We
stress that the monotonicity conditions built into the definition of
types need not be re-imposed as separate constraints: if (τ+, τ×)
is admissible as a type pair, then the intended ordering of sums and
products is consistent with some strictly increasing positive tuple, and
the additional inequalities a1 < ⋯ < a7
ensure that the induced tables respect the ambient coordinate order.
A small subtlety is that types are defined by comparisons among all
sums (respectively, products), while our reduced constraint set compares
only representatives. The equalities su = srk
for u ∈ Ck
ensure that every sum in block Ck equals its
representative sum, and the strict inequalities srk < srk + 1
ensure separation between distinct blocks. Consequently, any solution
satisfies
u ∈ Ck, v ∈ Cℓ, k < ℓ ⇒ su = srk < srℓ = sv,
and similarly for products. Thus a solution induces the specified weak
orderings; there is no possibility that two blocks collapse (that would
violate strict separation) or that an unprescribed equality appears
between different blocks (again violating strict separation). This is
the key point that lets us reduce type realizability to a finite,
checkable set of polynomial relations.
We next incorporate normalization. Over ℝ > 0 we may scale A by any c > 0 without changing the truth
of any comparison among sums or products: for sums the scaling
multiplies all values by c,
and for products it multiplies all values by c2. Therefore, in the
real feasibility problems we impose the normalization
a1 = 1.
This removes one degree of freedom and improves numerical conditioning
for solvers. It is also convenient to regard the remaining variables as
ratios xk = ak/a1,
so that x1 = 1 and
1 < x2 < ⋯ < x7;
however, in practice we keep the notation ak and simply
substitute a1 = 1
into all constraints. Over ℕ we do not
impose a1 = 1 a
priori, but we do enforce gcd (A) = 1 as a witness-reduction
convention once an integer solution is found; this does not affect
membership in SPP(7) and eliminates
redundant scaled copies.
The linear constraints coming from τ+ can be exploited further. Any equality ap + aq = ap′ + aq′ can be rewritten as a homogeneous linear relation among the variables, and the full set of addition equalities defines an affine subspace (after setting a1 = 1). We may therefore perform a symbolic elimination step: compute a row-reduced basis for the linear system, express a subset of the variables in terms of free parameters, and substitute into the remaining constraints. This reduces the dimension of the semi-algebraic set presented to the nonlinear solver and often dramatically decreases runtime. We do not require this elimination for correctness; it is a purely syntactic preprocessing step that preserves satisfiability.
Finally, we assemble the compatibility instance. Over ℝ > 0 it has the form
Φℝ(τ+, τ×) := (a1 = 1) ∧ (a1 < a2 < ⋯ < a7) ∧ ⋀k(ak > 0) ∧ Φ+(τ+) ∧ Φ×(τ×),
where Φ+(τ+)
is the conjunction of representative equalities and adjacent-block
strict inequalities for sums, and Φ×(τ×)
is the analogous conjunction for products. Over ℕ we replace the domain constraints by ak ∈ ℕ and omit
the scaling normalization. In either case, the resulting formula is
quantifier-free and consists only of strict order relations and
polynomial equalities/inequalities of degree at most 2. This is the exact form needed in the next
stage, where we enumerate candidate type pairs and use certified
decision procedures to decide whether Φℝ(τ+, τ×)
(and, when relevant, its integer analogue) is satisfiable.
For each target pair (i, j) ∈ [13, 28]2 ∩ ℤ2 we decide membership in SPPℝ > 0(7) by enumerating all candidate type pairs (τ+, τ×) with exactly i sum-classes and j product-classes and then deciding satisfiability of the associated real compatibility instance. The point of the real stage is twofold: it prunes many pairs (i, j) immediately (since ℕ ⊂ ℝ > 0), and it reduces the subsequent integer search to a small set of type pairs that are arithmetically plausible.
We represent a type τ+ (and similarly τ×) as an ordered
partition of I7 = {(p, q) : 1 ≤ p ≤ q ≤ 7}
together with the induced weak order consistent with the monotonicity
constraints
(p, q) ≺ (p + 1, q), (p, q) ≺ (p, q + 1)
whenever the indices are valid. To enumerate all types with a prescribed
number of blocks, we proceed by backtracking along a fixed linear
extension of the poset I7 (e.g. lexicographic
order on (p, q)). At
each step we assign the next index u either (i) to an existing block
that is not forced to be strictly larger than some previously placed
comparable element, or (ii) to a new block at the end of the current
ordered list. We maintain a union–find structure for the equivalence
relation ∼ (encoding equalities) and a
directed acyclic graph encoding the strict part of the order ≺ (encoding inequalities between blocks). If
adding the proposed identification creates a directed cycle, or violates
monotonicity relative to already-placed comparable indices, we
backtrack.
To enforce the class count we keep only completed partitions with exactly i blocks for τ+ and exactly j blocks for τ×. We also quotient by the obvious symmetries coming from relabeling within blocks and from the choice of representatives: we store each type in a canonical form (e.g. by the lexicographically least representative mapping from I7 to block indices consistent with the order). This canonicalization prevents repeated exploration of syntactically different but equivalent encodings.
Before pairing addition and multiplication types, we test each type for realizability over ℝ > 0 . This is inexpensive and eliminates a substantial fraction of the combinatorial output of the backtracking step.
For τ+, realizability is a strict linear feasibility problem after the normalization a1 = 1: the constraints are a1 = 1, 1 < a2 < ⋯ < a7, and the linear equalities/inequalities dictated by τ+. We decide feasibility by exact rational linear programming with strict inequalities handled by the standard ε-relaxation trick (replace x < y by x + ε ≤ y and search for a feasible ε > 0), or equivalently by finding a rational point in the relative interior of the resulting polyhedron. Infeasibility at this stage certifies that no compatibility instance using this τ+ can be satisfiable.
For τ×, realizability over ℝ > 0 is also reducible to strict linear feasibility by passing to logarithmic variables. Writing yk = log ak, equalities apaq = ap′aq′ become yp + yq = yp′ + yq′ and strict inequalities apaq < ap′aq′ become yp + yq < yp′ + yq′, while a1 < ⋯ < a7 becomes y1 < ⋯ < y7 and a1 = 1 becomes y1 = 0. Thus τ× alone is realizable if and only if a certain strict rational polyhedron in y-space is nonempty. We again decide this by exact linear methods. This filter is purely necessary (it ignores addition constraints) but very effective.
Fix (i, j) and let 𝒯+(i) (resp. 𝒯×(j)) denote the realizable addition (resp. multiplication) types with the required class count. The naive approach would solve every compatibility instance for every pair in 𝒯+(i) × 𝒯×(j). Instead we exploit two incremental pruning mechanisms.
First, for each τ+ ∈ 𝒯+(i) we perform the linear elimination described earlier and obtain an explicit parametrization of the affine subspace cut out by the addition equalities (after setting a1 = 1). Concretely, we express a subset of the variables as affine functions of free parameters t1, …, td, with d typically much smaller than 7. We then rewrite all remaining addition inequalities (including a1 < ⋯ < a7) as strict linear constraints in the t-variables, producing a finite union of relatively open rational polyhedral cones (depending on the branching introduced by strict inequalities). Any cone that is empty is discarded immediately.
Second, we add the multiplication constraints inside each surviving cone. We begin with the product equalities alone (degree-2 equations after substitution from the addition elimination) and test them by Gröbner-basis or resultant computations over ℚ whenever the dimension is small; contradictions here are common because the addition elimination often forces affine relations among the ak that are incompatible with multiplicative identifications. Only if this algebraic precheck does not refute the system do we introduce the strict product inequalities (adjacent-block separations) and pass to a full real decision procedure.
After preprocessing, each remaining compatibility instance is a quantifier-free formula in d real variables (the parameters) consisting of strict linear inequalities and quadratic polynomial equalities/inequalities. We decide satisfiability using a certified real-algebraic solver, with two complementary goals: if the formula is satisfiable we must extract a checkable witness point; if it is unsatisfiable we must extract a checkable refutation.
On the satisfiable branch, CAD-style methods provide a sample point in each feasible cell. We record the sample point as either a rational tuple (when one is found) or as an algebraic tuple represented by squarefree minimal polynomials together with isolating intervals. The verification step is independent: given the recorded data, a standalone checker evaluates each polynomial constraint exactly in the real-closed field of algebraic numbers (or by exact interval arithmetic with separation bounds) to confirm that all equalities hold and all strict inequalities are satisfied. This produces a bona fide certificate that (τ+, τ×) is realizable over ℝ > 0, hence that (i, j) ∈ SPPℝ > 0(7).
On the unsatisfiable branch, we require a proof artifact rather than a mere ``UNSAT’’ flag. In practice we use two independently checkable formats: (i) a CAD refutation in which the projection set and the sign-invariance information suffice to certify that no cell satisfies the constraints, and (ii) an SMT-style derivation trace (e.g. a sequence of validated theory lemmas in the theory of real-closed fields) whose individual arithmetic steps can be replayed by a small proof checker. We accept nonexistence for a type pair only when at least one such artifact is produced and verified.
For each (i, j) we obtain a finite list of type pairs (τ+, τ×) that are realizable over ℝ > 0, each accompanied by a verified witness point, and we certify that all remaining pairs are unrealizable by verified refutations. If no type pair survives, then by inclusion ℕ ⊂ ℝ > 0 we conclude immediately that (i, j) ∉ SPP(7). Otherwise, the surviving real-realizable type pairs form the input to the next stage, where we determine whether any real realization can be lifted to an integer witness or whether integrality is provably obstructed.
Fix a target pair (i, j) and consider the finite list of type pairs (τ+, τ×) that survive the real stage, i.e. those for which the real compatibility instance is satisfiable. For each such pair we must decide whether there exists an realization, and we must do so with independently checkable artifacts. Conceptually we separate the task into (a) producing an integer witness whenever one exists and (b) certifying that every real realization is necessarily nonrational (hence cannot come from integers) when no witness exists.
The lifting problem is most naturally posed in the normalized space
used in the real stage. Indeed, if A = {a1 < ⋯ < a7} ⊂ ℕ
realizes (τ+, τ×),
then the scaled tuple
$$
\left(1,\frac{a_2}{a_1},\dots,\frac{a_7}{a_1}\right)\in\mathbb{Q}_{>0}^7
$$
(with the same strict order) realizes the type pair over ℝ > 0 after imposing a1 = 1. Conversely, if
the normalized compatibility instance admits a rational solution (1, r2, …, r7) ∈ ℚ > 07,
then clearing denominators produces an integer witness: writing D = lcm(den(rk))
and setting A = {D, Dr2, …, Dr7}
yields A ⊂ ℕ with identical
addition and multiplication collision patterns. The verification is
immediate: multiplying all variables by a positive constant preserves
strict inequalities, and it preserves equalities/inequalities among all
pairwise sums and products because
(Dap) + (Daq) = D(ap + aq), (Dap)(Daq) = D2(apaq).
Thus the integer lifting question reduces to the existence of solutions
of the normalized compatibility instance. This reduction is the basis
for both our witness production and our nonexistence certificates.
Each real-realizable type pair comes with a certified sample point from the decision procedure of the real stage, represented either as a rational tuple or as an algebraic tuple (minimal polynomials with isolating intervals). When the sample point is rational we immediately obtain an integer witness by clearing denominators, and we record both the normalized rational tuple and the resulting integer set. When the sample point is algebraic, we treat it as evidence of feasibility but not yet as an obstruction: we must still determine whether point in the same semi-algebraic feasible region is rational.
Our first attempt is a rational reconstruction step guided by the
structure already computed in the real stage. After eliminating the
linear constraints from τ+ (and a1 = 1), we have an
explicit affine parametrization
$$
a_k=\alpha_k+\sum_{r=1}^d \beta_{k,r} t_r,\qquad
\alpha_k,\beta_{k,r}\in\mathbb{Q},
$$
together with a finite union of open rational polyhedral cones in the
parameter space enforcing the remaining strict linear inequalities
(including 1 < a2 < ⋯ < a7
and the strict sum inequalities). Substituting this parametrization into
the product equalities of τ× yields a system of
quadratic equations in t1, …, td
over ℚ. We then search for a rational
point (t1, …, td) ∈ ℚd
satisfying both the quadratic equalities and the open cone inequalities.
Any rational solution in parameter space yields a rational solution in
a-space, hence an integer
witness.
Although the feasible region is a priori unbounded (scaling invariance in the integer world translates to losing the a1 = 1 normalization), the normalized system typically has very small algebraic dimension once both τ+ and τ× are imposed. In practice we frequently encounter a 0-dimensional or 1-dimensional solution set in parameter space. This permits a bounded-denominator strategy that is both effective and certifiable.
Concretely, we clear denominators in all substituted equations to obtain quadratic polynomials F1, …, Fm ∈ ℤ[t1, …, td] and strict linear inequalities Ls(t) > 0 with Ls ∈ ℤ[t]. We then enumerate rational tuples tr = pr/q with a common denominator q ≤ B, where B is an explicit search bound determined from the linear parametrization (least common multiple of the denominators of αk, βk, r and, when d is small, auxiliary bounds obtained from elimination of the quadratic system). For each candidate, we check Fℓ(t) = 0 exactly in ℚ and verify Ls(t) > 0 exactly by sign computation. Whenever a candidate succeeds we construct the integer witness by clearing denominators in (a1, …, a7) and record a certificate consisting of the rational tuple and the scaled integer tuple. A standalone checker re-evaluates all equalities/inequalities and recomputes (|A + A|,|AA|) directly from the integer witness.
We emphasize that the bounded-denominator search is used only as a mechanism. Failure of this search is never taken as evidence of nonexistence; it merely triggers the obstruction analysis described next.
When no rational point is found, we certify nonexistence of integer realizations by proving that real solution of the normalized compatibility instance has at least one irrational coordinate. Since any integer realization would yield a rational normalized realization, such a certificate rules out A ⊂ ℕ for that type pair.
The obstruction proof proceeds by exact elimination on the reduced
parameter system. In the common 0-dimensional case, we compute a univariate
elimination polynomial P(x) ∈ ℤ[x] for a
chosen coordinate or ratio (e.g. x = ak/aℓ
or x = tr),
together with a derivation (e.g. a Gröbner-basis trace) showing that any
real solution forces P(x) = 0. We then certify
that P has no rational root.
For quadratic obstructions this reduces to a discriminant argument: if
x satisfies
x2 + ux + v = 0, u, v ∈ ℚ,
and the discriminant u2 − 4v is not a
square in ℚ, then x ∉ ℚ. In higher degree, we certify
the absence of rational roots by the rational root test (after content
normalization) and, when needed, certify irreducibility by a modular
reduction check (exhibiting a prime p for which P mod p is irreducible).
The resulting artifact consists of (i) the polynomial P, (ii) the elimination trace
linking P to the original
constraints, and (iii) the arithmetic proof that P has no linear factor over ℚ. A checker verifies each step using exact
integer arithmetic and polynomial remainder computations.
In the less frequent case where the solution set has positive dimension, we do not assume irrationality from the presence of an algebraic sample point. Instead, we either exhibit a rational point by parametrization of the corresponding conic/curve (again with exact inequality checking), or we refine the elimination until we isolate a forced irrational parameter (for instance, a ratio constrained to lie in a singleton algebraic extension). This is precisely the phenomenon anticipated by the irrational obstruction patterns: the type constraints can force a rigid multiplicative relation incompatible with rationality.
For fixed (i, j), we apply the above lifting analysis to every surviving real-realizable type pair. If at least one type pair yields a rational normalized solution, we output an explicit integer witness set A ⊂ ℕ for (i, j). If every surviving type pair is shown to be real-only via an irrational obstruction certificate, then we conclude that (i, j) ∉ SPP(7) despite belonging to SPPℝ > 0(7). Finally, if the real stage produced no surviving type pair at all, nonmembership in SPP(7) follows immediately by inclusion ℕ ⊂ ℝ > 0.
All outputs are recorded in a uniform certificate format: witnesses are stored as explicit integer sets together with their computed invariants, and nonexistence claims are stored as a finite list of eliminated type pairs, each eliminated either by a real refutation (from the previous stage) or by a rational-obstruction proof as above. These artifacts are exactly what we use in the final stage to tabulate SPP(7) and to resolve the remaining candidate pairs.
We now assemble the outputs of the type enumeration, the real
feasibility stage, and the integrality lifting stage into an exact
description of
SPP(7) = {(|A + A|,|AA|) : A ⊂ ℕ, |A| = 7}
within the a priori range [13, 28] × [13, 28]. Let
S := SPP(7) ∩ ([13, 28]2 ∩ ℤ2).
By Lemma~1 and Lemma~2, membership of a fixed (i, j) is decided by a
finite family of compatibility instances indexed by the type pairs (τ+, τ×)
with class counts (i, j). For each such
instance we either (i) exhibit a rational normalized solution and hence
an integer witness set A ⊂ ℕ,
or (ii) certify that no real solution exists (hence no integer
solution), or (iii) certify that all real solutions are necessarily
nonrational, whence no integer solution exists. Taking the union over
all type pairs for all (i, j) ∈ [13, 28]2
produces exactly the finite set S together with independently
checkable certificates for each inclusion and exclusion, as asserted in
Theorem~A.
For readability we present S in two complementary formats. First, Table~ gives a membership grid for the square [13, 28]2: a marked cell at coordinates (i, j) indicates (i, j) ∈ S. Second, the machine-readable list of all pairs in S, together with a pointer to the corresponding witness/certificate artifact, is included in the archived output (and is used by the standalone verifier in 8). The LaTeX table and the machine-readable list are generated from the same certificate database, so that the printed tabulation is not a manually curated object.
It is useful to distinguish three logically different ways in which a cell can be unmarked. If no type pair with class counts (i, j) is realizable over ℝ > 0, then nonmembership in SPP(7) is immediate from ℕ ⊂ ℝ > 0. If some type pairs are realizable over ℝ > 0 but each is eliminated by an irrational-obstruction certificate, then (i, j) ∉ SPP(7) despite lying in SPPℝ > 0(7). Finally, if at least one type pair admits a rational normalized solution, then (i, j) ∈ SPP(7) and we record a concrete integer witness.
The computed set S necessarily lies within the classical bounds 2n − 1 ≤ |A + A| ≤ n(n + 1)/2 and 2n − 1 ≤ |AA| ≤ n(n + 1)/2 (here n = 7), hence within [13, 28]2. Our output reproduces the expected boundary points corresponding to standard structured examples, which serve as consistency checks for the end-to-end pipeline.At the opposite extreme, Sidon-type constructions yield |A + A| = 28 by definition, and our tabulation records the corresponding range of achievable |AA| values at |A + A| = 28. Dually, multiplicatively Sidon (or near-multiplicatively-Sidon) behaviour pushes |AA| toward 28, and we record the associated achievable sumset sizes at |AA| = 28. These ``edge slices’’ of Table~ are a convenient way to see how additive and multiplicative structure trade off at fixed n.
Beyond extremal points, the computed set S exhibits two qualitative features that are visible directly in the membership grid and in the plotted point cloud (Figure~). First, there is a pronounced concentration of realizable points along a narrow vertical run at small |A + A| values, corresponding to sets that are close (in the sense of addition-table type) to an arithmetic progression. We refer to this visually as the . Combinatorially, these points arise from addition types τ+ with many forced sum collisions; once τ+ is fixed, the remaining degrees of freedom allow a variety of multiplicative collision patterns, producing a visible spread in |AA| even when |A + A| is near its minimum.
Second, near the diagonal |A + A| ≈ |AA| we observe a sparse but nonempty collection of points in which both invariants are simultaneously small. This is the region that heuristically corresponds to the ``smallest extremal zone’’ (SEZ) for n = 7, i.e. the lower-left portion of [13, 28]2 in which max {|A + A|,|AA|} is close to its minimum possible value. Our computation determines the exact Pareto-minimal subset of S (those pairs not dominated in both coordinates by another realizable pair) and provides witnesses for each such frontier point. In particular, the point (18, 18) above lies on this frontier and illustrates how mixed additive/multiplicative structure (here, mild additive compression together with many multiplicative collisions) can outperform both pure arithmetic and pure geometric progressions with respect to the objective max {|A + A|,|AA|}.
We now isolate the four candidate pairs
(21, 18), (18, 20), (18, 21), (19, 20),
which were not settled by earlier methods for n ≤ 6 and which, for n = 7, lie in the delicate
transition regime where neither sumset-minimality nor
productset-minimality dominates. For each of these pairs, our
computation enumerates all type pairs (τ+, τ×)
with the required class counts, discards those refuted over ℝ > 0, and then applies the
integrality lifting analysis to the remaining real-realizable cases. The
outcome is unconditional: each pair is either realized by an explicit
A ⊂ ℕ, or else is excluded by
a finite list of solver-verifiable refutations/obstructions covering
every compatible type pair.
For compactness, Table~ records, for each of the four pairs, the decision (in/out of SPP(7)) together with a pointer to the corresponding artifact: either a witness file containing an explicit integer set A and a recomputable evaluation of (|A + A|,|AA|), or a bundle of nonexistence certificates eliminating all surviving real types for that pair. The artifacts referenced in Table~ are precisely those verified in the reproducibility step of 8.
Combining the full membership grid (Table~) with the witness/certificate artifacts referenced therein yields the promised exact identification of SPP(7) ∩ ([13, 28]2 ∩ ℤ2). Every positive cell is backed by a concrete integer witness set and a recomputation of its invariants, and every negative cell is backed by a finite disjunction of eliminated type pairs whose refutations are checkable independently of the original solver environment. We now turn to the verification layer: the certificate format, the standalone checker, cross-validation across independent implementations, and the archiving of all types and instances.
The preceding section reduces the determination of S to a finite collection of concrete claims of two forms: (a) , i.e. an explicit A ⊂ ℕ realizing a given pair (|A + A|,|AA|); and (b) , i.e. the unsatisfiability (over ℝ > 0 or over ℕ) of every compatibility instance attached to the relevant type pairs. In order for these claims to constitute a proof rather than a computation log, we require that each claim be accompanied by an artifact that can be checked independently of the original implementation and, crucially, independently of any heuristic choices made during search.
We therefore organize the output as a indexed by type pairs (τ+, τ×) (and hence, by Lemma~1, also by their class counts (i, j)). Each record contains (i) a canonical encoding of τ+ and τ×; (ii) the induced normalized compatibility instance as an explicit quantifier-free formula in the variables a1, …, a7; and (iii) either a witness realization (existence) or a refutation/obstruction object (nonexistence). The verifier described below accepts the record as input and outputs using only exact arithmetic and certified algebraic-number primitives.
To prevent ambiguity, we fix a canonical labeling of I7 = {(i, j) : 1 ≤ i ≤ j ≤ 7} by lexicographic order and represent each type as:The monotonicity constraints inherent in the definition of type are checked by the verifier directly from this encoding. From the type, we generate the compatibility instance deterministically: every equality block yields polynomial equalities (ai + aj = ak + aℓ for τ+ and aiaj = akaℓ for τ×), every strict order relation yields a strict inequality, and we append the ambient constraints 1 = a1 < a2 < ⋯ < a7 and ai > 0. (When testing integer feasibility, the integrality requirement is treated separately, so that the same real instance can be reused as a pruning stage.)
To ensure that the printed tables in 7 are not a hand-edited byproduct, we also store for each instance a short containing hashes of the type encodings and of the generated constraint list. The LaTeX tables and plots are produced by reading this manifest, so that any discrepancy between displayed data and verified data would be detected at the build stage.
An existence certificate consists of a concrete integer set A = {a1 < ⋯ < a7} ⊂ ℕ together with the claimed pair (i, j) and a pointer to at least one type pair (τ+, τ×) that A induces. The independent checker verifies:No auxiliary information is needed: the certificate is simply the explicit witness, and correctness reduces to a deterministic computation. In particular, when a rational normalized solution is found at the real-feasibility stage, Lemma~5 is implemented explicitly by clearing denominators and rechecking the induced type after scaling, so that the witness is already in the integer domain at verification time.
For nonexistence we separate two logically distinct situations. First, for many type pairs the real compatibility instance is unsatisfiable over ℝ > 0. For these cases we store a . Operationally, the solvers we use (a CAD-based engine and an SMT(NRA) engine) can both return a derivation trace that proves unsatisfiability; however, solver traces are rarely standardized in a way that makes them robust across versions. We therefore convert each solver-dependent trace into a solver-independent certificate of the following form:The checker verifies sign-invariance data by exact univariate root isolation and subresultant computations along the cylinder structure, and then evaluates the original constraints at each certified sample point. Since every point in a cell shares the same relevant sign conditions, falsification at the sample point implies falsification on the entire cell, and coverage of the decomposition implies global unsatisfiability. This certificate format is larger than a bare flag, but it is stable, self-contained, and does not presuppose trust in any particular solver.
Second, some type pairs are realizable over ℝ > 0 but admit no rational solutions; by Lemma~5 this implies the absence of integer witnesses. For these cases we store an that isolates a specific algebraic parameter forced by the constraints. Concretely, after eliminating linear degrees of freedom coming from τ+, the remaining multiplicative equalities often force a ratioThe verifier checks each identity in exact arithmetic and thereby concludes that any rational realization would force a rational root of P, which is impossible.
All certificates are verified by a standalone checker whose trusted core consists of exact integer/rational arithmetic, polynomial gcd and subresultant routines, and certified univariate root isolation (Sturm sequences). The checker does call external solvers. For convenience, it can also regenerate the compatibility instance from the stored type encodings and confirm that the stored instance matches the regenerated one via hash comparison; this prevents accidental divergence between the enumerator and the verifier.
To minimize hidden nondeterminism, the enumeration of types, the normalization conventions (e.g. a1 = 1), and the ordering of constraints are fixed once and for all, and every produced artifact includes a versioned header recording the generator commit hash and a content hash of the instance. The build that produces Tables~ and~ runs the checker over the full certificate database and fails if any record does not verify.
We additionally cross-validate the computational stage by running two independent solver stacks on every real-feasibility instance: one CAD-based and one SMT-based, each producing its own raw trace. A refutation is accepted into the database only after both stacks agree on the truth value, and only after the agreed trace is converted into a solver-independent certificate as above. For existence, the two stacks are used only as search aids; correctness is discharged solely by the witness verification.
The archived artifact bundle contains: (i) the complete list of type pairs considered, including symmetry reductions; (ii) for each type pair, the generated normalized constraint instance; (iii) for each realizable pair, at least one integer witness file; (iv) for each unrealizable type, either a CAD-style real refutation certificate or an irrational-obstruction certificate; and (v) a manifest linking every entry to the corresponding table cell in 7. This closes the verification layer needed for Theorem~A and sets up a clean interface for extensions in 9, where the primary issue becomes not correctness but scalability of enumeration and certification as n grows.
Theorem~A should be read less as an isolated classification for n = 7 and more as a demonstration that SPP(n) can be decided by reducing it to a finite family of certified semi-algebraic feasibility problems attached to type pairs (τ+, τ×). The immediate question is how far this approach can be pushed as n increases, and how robustly it adapts when one changes the ambient domain (from ℕ to ℝ > 0, to ℕ0, or to ℤ). We record here what appears to be feasible with current methods, what bottlenecks become dominant, and how one can aim the same pipeline at the region of parameter space that has historically been hardest to control.
Two sources of combinatorial growth are intrinsic. First, the table index set In = {(i, j) : 1 ≤ i ≤ j ≤ n} has size n(n + 1)/2, so the raw number of sum (or product) entries is 36 for n = 8 and 45 for n = 9, compared to 28 for n = 7. Second, the number of weak orderings on In compatible with the monotonicity constraints grows rapidly. In practice, however, we do not enumerate all types: for each candidate pair (i, j) we need only those types whose numbers of equivalence classes match i and j (Lemma~2), and we can restrict further by easy necessary constraints (e.g. the Freiman-type constraints implicit in very small |A + A|, or the rigidity of very small |AA| for positive reals). The computational burden therefore shifts to : identifying a finite candidate family large enough to be complete, while keeping it small enough that certified feasibility checks remain tractable.
For n = 8, the most realistic goal is not a full determination of SPP(8) over the entire square [15, 36]2, but rather completeness in restricted regimes: a strip near the lower envelope (small |A + A| or small |AA|), or a bounded region for max {|A + A|,|AA|}. For n = 9 the same philosophy appears necessary: the basic pipeline remains valid, but full coverage would require either a major new symmetry reduction for types or a fundamentally faster certification layer.
A key structural advantage of the present approach is that τ+ contributes only linear constraints, and therefore partitions the normalized realization space into polyhedral pieces (Lemma~3). For n = 8, 9, we expect this to remain the primary pruning mechanism: one first enumerates plausible addition types τ+ with a fixed class count |A + A| = i, then for each cone (or relatively open polyhedron) coming from τ+ one checks which multiplication types τ× can be compatible at all. This is not merely a practical tactic; it also aligns with the typical rigidity phenomenon that ``few sums’’ forces strong additive structure, thereby drastically constraining the relative positions of the ai. In implementations, this suggests separating the pipeline into (i) polyhedral enumeration and redundancy elimination for τ+, carried out with exact rational arithmetic; (ii) multiplicative constraint generation and simplification on each polyhedral chamber; and only then (iii) certified real feasibility.
A further, largely unexplored optimization is to exploit implied by τ× without invoking CAD. For example, if τ× forces many equalities of the form aiaj = akaℓ, then after normalization one often obtains equalities among ratios au/av, i.e. multiplicative relations in a low-dimensional torus. Detecting these relations early and simplifying the instance (e.g. by substituting a parametrization when the relations define a rank-one subgroup) can reduce the degree and number of polynomials passed to the certified solver stage.
The real-feasibility stage is the first point at which worst-case
complexity is doubly exponential in the number of variables, and
therefore it becomes critical to reduce dimension before calling a full
decision procedure. For n = 7
this reduction is already present implicitly (by normalization and by
the linear structure induced by τ+). For n = 8, 9 it is essentially
mandatory. Concretely, once τ+ has been fixed, we can
choose an affine coordinate system on each polyhedral chamber so that
only d ≪ n free
parameters remain. One then expresses the multiplicative constraints in
these parameters and runs CAD/SMT on the reduced system. This changes
the certification burden from
hard in $7$ variables'' tomoderate in d variables, repeated many times,’’
which is more amenable to parallelization and to caching of projection
polynomials. We also expect that incremental SMT(NRA) solvers will be
useful as engines, provided that the final artifacts are converted to
solver-independent certificates as in 8.
As n grows, the proportion of real-feasible instances that fail to lift to integers may increase, simply because there are more degrees of freedom for irrational obstructions (Lemma~6) to arise. For this reason, it becomes important to systematize the integer-lifting stage rather than treating it as an ad hoc search for witnesses. Two directions seem promising. First, in rationally realizable cases, one can attempt to a rational parametrization by identifying a maximal set of independent multiplicative equalities whose solutions form a rational torus, and then clearing denominators (Lemma~5). Second, in the non-liftable cases, one should aim to automatically extract a low-degree obstruction polynomial P(x) for some forced ratio x = au/av, together with a certificate that P has no rational root. Both directions fit naturally into the certificate framework: they produce either an explicit integer witness or an explicit irrationality proof.
The extension to SPPℝ > 0(n) is conceptually straightforward: we simply omit integrality, retain positivity, and interpret types exactly as before. The main new phenomenon is that scaling invariances become more prominent; for ℝ > 0 it is often useful to normalize both a1 = 1 and one additional parameter (for instance, fix a2 or fix a7) to avoid continuous families of equivalent solutions. For ℕ0 (allowing 0) and for ℤ, one must revisit monotonicity and sign constraints for τ×. Over ℕ0, products can collapse via 0, leading to additional collision patterns not present over ℕ; this can be handled by introducing a distinguished ``zero’’ symbol and splitting into cases according to whether 0 ∈ A. Over ℤ, signs destroy the simple monotonicity of products, so a multiplication-table type must encode order information in a way that is compatible with sign changes (or else avoid ordering and record only equalities). A pragmatic approach is to treat ℤ by reducing to finitely many sign patterns (how many negatives occur) together with absolute values, since |ab| = |a||b| restores positivity at the cost of extra combinatorial branching. In all cases, the guiding principle remains the same: we enumerate combinatorial collision patterns and discharge each case by a certified feasibility/refutation artifact.
The method is well suited to regimes in which neither |A + A| nor |AA| is extremal, precisely
because types allow one to isolate fine collision structures without
assuming global structure such as
$A$ is an arithmetic progression'' orA is a geometric progression.’’ In
the classical sum–product landscape, the hardest instances tend to lie
near the diagonal where |A + A| and |AA| are both moderately
small, and where known general inequalities do not decisively push one
quantity large when the other is small. For fixed n, this manifests as a ``river’’ of
candidate pairs (i, j) that are not
immediately ruled out by extremal arguments. Our pipeline turns the
informal difficulty of this region into a finite, checkable list of type
pairs. Thus, for n = 8, 9, an
attainable and meaningful goal is : for a chosen bound M, decide all pairs with max {|A + A|,|AA|} ≤ M
(or with |A + A|+|AA| ≤ M)
by exhaustive type enumeration within that strip. This provides a
rigorous map of the difficult region at small n, and it produces data that can
inform conjectures about the shape of the feasible set as n grows.
In summary, the proof architecture of 6–8 appears stable under these extensions: types reduce the problem to finitely many explicit instances; ℝ > 0 feasibility provides strong pruning; integer existence is recovered by rational lifting or refuted by explicit irrational obstructions; and every outcome is packaged as an independently checkable certificate. The main open challenge is not logical but computational: designing enumeration and simplification steps that keep the certified feasibility layer within reach for n = 8, 9, at least in the targeted strip regimes where the ``river’’ is concentrated.