Seventy elements for the parameter-five cyclic carrier
Abstract
The complete original zero-support classification determines the parameter-five cyclic minimum.
Theorem 1.1 (Seventy elements are necessary and sufficient for a cyclic carrier at m = 5).
Lean statement: D5/S3/Combinatorics/Sequenceability/OriginalCyclicFiveCarrierLowerBound.cyclic_five_carrier_card_lower_bound
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/OriginalCyclicFiveCarrierLowerBound.cyclic_five_carrier_card_lower_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let G be a finite commutative additive group that is cyclic, and let f label the original Coordinate 5 in G. Assume that f(q) has additive order exactly five and that, for every finite set C of original coordinates, C is nonempty and its labels sum to zero if and only if C is one of the four triples {q,a_i,b_i}, indexed by Fin 4. Then Nat.card G is at least 70. Neither label injectivity nor a separate nonzero-label assumption is required.
Put Q = f(q), H = the subgroup generated by Q, and K = G/H. The prescribed triples give f(a_i)+f(b_i) = -Q, while Nat.card H = 5. The earlier cyclic lower bound implies Nat.card K at least ten. The four classes A_i represented by f(a_i) are nonzero and occupy distinct orbits under negation.
The stronger obstruction uses three distinct pairs. More generally, when m is at least four, choose one original coordinate from each of three distinct pairs. Their label sum cannot lie in the subgroup generated by Q. To see this, write a putative sum as t*Q with 0 <= t < m. If t <= m-4, adjoin t whole pairs from the remaining indices. If t = m-1, adjoin q. If t = m-3, replace all three selected coordinates by their mates; if t = m-2, make that replacement and adjoin q. In each case the resulting nonempty zero support contains three singly selected pairs and is not one prescribed triple. Thus no signed sum of three A-classes at different indices is zero in K.
Suppose K had n elements with ten at most n and n at most thirteen. Identify the cyclic quotient with ZMod n and replace each A_i by its representative in the same negation orbit between one and n/2. Ordering the four distinct representatives gives 1 <= a < b < c < d and 2d <= n. The integer inequalities force one of a+b=c, a+b=d, a+c=d, b+c=d, a+b+c=n, a+b+d=n, a+c+d=n or b+c+d=n. Each equality gives a forbidden signed sum of three distinct A-classes. Therefore Nat.card K is at least fourteen, and Nat.card G = 5Nat.card K is at least seventy.
The lower bound is attained in ZMod 70. Label q by 14, p by 48, and the four ordered pairs (a_i,b_i) by (1,55), (9,47), (17,39) and (63,63). The q label has additive order five, and the only nonempty coefficient-one zero supports among all subsets of the ten original coordinates are the four prescribed triples. Combining this realization with the lower bound determines the smallest cyclic carrier at m = 5 to have seventy elements. It gives no minimum for arbitrary finite abelian carriers or for other parameters.