Strong integer orderings
Abstract
Integer orderings with no proper nonempty zero-sum interval.
Theorem 1.1 (Every finite nonzero integer set has a strong ordering).
Lean statement: D5/S1/Words/Sequenceability/IntegerStrongOrdering.exists_integer_strong_ordering
Proof. Machine-checked in Lean as D5/S1/Words/Sequenceability/IntegerStrongOrdering.exists_integer_strong_ordering (✓ std3). ∎
Citation. Noah Kravitz (2024). Rearranging small sets for distinct partial sums. DOI: 10.48550/arXiv.2407.01835.
Commentary.
For every finite set A of integers excluding zero, there is a list w permuting A.toList. For every pair of natural indices i < j with j at most the length of w, the sum of take (j-i) (drop i w) is nonzero whenever i is nonzero or j is not the full length. Only the complete word is exempt. Empty sets, singleton sets, either empty sign block and equal positive and negative totals are included.
The private construction simultaneously orders positive sets P and N so equal bounded prefix sums occur only at the empty pair or the full pair. Strong induction on card(P)+card(N) allows either side to become the larger-total side at each call. For a side with at least two elements, cancellation shows that at most one deletion leaves the opposite total. Delete another element, recurse and append it. Its deletion inequality removes the old full-pair collision, and total dominance excludes a new collision with a proper prefix.
The final word is reverse(p) followed by map neg n. Positive-prefix strictness handles intervals within either sign block. A cross-block collision is exactly an equality between the constructed positive prefixes and forces the initial and final endpoints. Prefix splitting gives the full interval claim. Distinctness is within each positive set; cross-sign shared magnitudes are allowed.
This formalizes Kravitz, Theorem 1.3 and Remark (1), arXiv:2407.01835v2, pages 2-3. Kravitz credits a similar route to Sawin’s 2015 MathOverflow contribution. The result is known mathematics. The retained construction supplies an unbounded simultaneous recursion absent among the inspected formal suppliers. It does not solve the arbitrary abelian-group or integral-primitive target, and implements no ordered-kernel extension.
The escape registration remains unfinished (declared_unresolved, source-equivalence): forbidden_dependency under source.unsafe_or_external at Nat.pow. The faithful Reg family proofs compile, but an accepted source-binding certificate is missing. See https://github.com/the-omega-institute/trureturing/issues/20106.