Triple-product sum rigidity
Abstract
Equal triple products in a sufficiently short positive integer interval have equal sums.
Theorem 1.1 (Integer sum rigidity).
Proof. Machine-checked in Lean as D5/S3/Arith/ShortIntervals/TripleProductSumRigidity.triple_product_sum_rigidity (✓ std3). ∎
Source. Repository-derived.
Commentary.
All eight variables are integers. Each of the six rows lies in the same closed interval. Repetitions, shared rows and arbitrary row order are allowed; the equality of sums is a conclusion.
Choose a least member x of each triple and write the other members as x+r and x+s. The cubic defect is 9x(r^2-rs+s^2)+(r+s)^3. For positive width it lies between zero and 9mh^2+17h^3, strictly below 26m^2. Distinct integer sums at least 3m have cube difference greater than 27m^2. Equal products make that cube difference a difference of defects, which is impossible. At zero width every row equals m.
The stronger predicate m>(h+1)^2 implies the square threshold here. This theorem leaves the classification of six-row unit relations, Hall conditions, complete-hull compositeness, higher-endpoint sectors, nonunit relations, larger cores, long spans and unrestricted Grimm’s conjecture unresolved.
References
- Truth anchor:
D5/S3/Arith/ShortIntervals/TripleProductSumRigidity.triple_product_sum_rigidity