Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A quadratic carrier lower bound from the original zero supports

Abstract

The full original zero-support classification forces a quadratic lower bound on the finite carrier.

Theorem 1.1 (At least m(m+1) elements are necessary).*

Lean statement: D5/S3/Combinatorics/Sequenceability/OriginalSharpnessCarrierLowerBound.carrier_card_lower_bound

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/OriginalSharpnessCarrierLowerBound.carrier_card_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let G be any finite commutative additive group, let m be a natural number with m at least two, and let f map the original Coordinate m into G. Write J = Fin(m-1), q and p for the two distinguished coordinates, and a_i,b_i for the paired coordinates indexed by J. Assume that f(q) has additive order exactly m. Assume also the complete coefficient-one zero-support classification: for every finite set C of original coordinates, C is nonempty and its f-labels sum to zero if and only if C is precisely {q,a_i,b_i} for some i in J. Then m*(m+1) is at most Nat.card G. No separate injectivity, nonzero-label or cyclicity hypothesis is imposed.

Put Q = f(q), P = f(p), A_i = f(a_i), B_i = f(b_i), and H = the additive subgroup generated by Q. Each prescribed triple gives Q+A_i+B_i = 0, hence A_i+B_i = -Q. The exact order assumption gives Nat.card H = m.

The full classification forces the cosets represented by 0, all m-1 values A_i, and P to be pairwise distinct in G/H. To exclude a collision, express the resulting relation as a residue multiple of Q and complete it with a suitable set of distinct a_j,b_j pairs and, when needed, q. The relation then produces a nonempty zero support outside the prescribed triple family. A collision involving the sentinel yields a forbidden support containing p; the A-coset collisions are ruled out by the corresponding paired completions. The argument includes the boundary case m = 2.

Thus Option(Option J) injects into G/H: none represents the zero coset, some none represents P, and some(some i) represents A_i. This domain has exactly m+1 elements, so Nat.card(G/H) is at least m+1. Translation by H partitions G into its orbits, namely these cosets, each of cardinality m. The finite quotient-cardinality identity therefore gives m*(m+1) at most Nat.card G.

The result applies to every finite commutative additive carrier satisfying the exact original support classification. The explicit cyclic construction of OriginalPolynomialCyclicOrderSharpness supplies a carrier with m*(6*m-7) elements under the same order and zero-support requirements. Together these pin quadratic growth for this complete support pattern. Merely attaining m-1 intersection-graph components in an arbitrary configuration does not supply the hypotheses of this lower bound. The exact smallest carrier size for general m remains undetermined.

At m = 3 the lower bound is attained without injective labels. Take G = ZMod 3 × (ZMod 2 × ZMod 2), with q labelled (1,(0,0)), p labelled (2,(1,1)), a_0 and b_0 both labelled (1,(1,0)), and a_1 and b_1 both labelled (1,(0,1)). The q label has additive order three, and the nonempty zero supports are exactly the two original triples. This group has twelve elements, equal to 3*(3+1), so equality holds at m = 3. This example establishes neither equality for every m nor a minimum among cyclic carriers.

Theorem 1.2 (At least 2mm elements are necessary for a cyclic carrier).

Lean statement: D5/S3/Combinatorics/Sequenceability/OriginalSharpnessCarrierLowerBound.cyclic_carrier_card_lower_bound

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/OriginalSharpnessCarrierLowerBound.cyclic_carrier_card_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The cyclic strengthening assumes a finite commutative additive group G that is cyclic, a natural number m at least two, and an arbitrary labeling f of the original Coordinate m. Its hypotheses are exactly addOrderOf(f(q)) = m and the complete coefficient-one zero-support classification: 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 original triples {q,a_i,b_i}, indexed by Fin(m-1). The conclusion is 2mm at most Nat.card G, without a label-injectivity or separate nonzero-label assumption.

Put Q = f(q), P = f(p), A_i = f(a_i), B_i = f(b_i), H = the subgroup generated by Q, and K = G/H. The prescribed triples give A_i+B_i = -Q, and H has m elements. The quotient K is finite cyclic. The generic argument already separates the classes 0, P and all A_i: every A_i is nonzero, different indices have different A-classes, and P avoids 0 and every A_i.

The complete support classification also excludes P+A_i from H. If P+A_i = tQ with 0 <= t < m and t <= m-2, complete {p,a_i} with t distinct whole a_j,b_j pairs outside index i. Its sum is zero, but a support containing p cannot be a prescribed triple. If t = m-1, the forbidden zero support is {q,p,a_i}. Thus P avoids every negative A-class as well.

For distinct indices i,j, the same completion method excludes A_i+A_j from H. Such indices require m at least three. Write a putative sum as tQ with 0 <= t < m. If t <= m-3, adjoin t whole pairs outside i,j to {a_i,a_j}; the resulting zero support lacks q. If t = m-2, {b_i,b_j} has sum -mQ = 0. If t = m-1, {q,a_i,a_j} has sum mQ = 0. None is a prescribed triple, so no A-class can equal the negative of an A-class at a different index.

Consequently the signed set S = {0,P} union {A_i,-A_i : i in Fin(m-1)} has no collisions except possibly A_i = -A_i at an individual index. A finite cyclic quotient has at most one nonzero element fixed by negation; when present, this is its unique element of additive order two. If r counts the self-negative A-classes, then r <= 1 and S has 2+2*(m-1)-r elements, at least 2m-1.

Let n = Nat.card K. If n is even, n >= 2m-1 rounds up to n >= 2m. If n is odd, K has no nonzero element fixed by negation, so r = 0 and S itself has 2m elements. This includes m = 2, where there is only one A-class and no distinct-index case to consider. Translation by H partitions G into cosets, each of cardinality m. Hence Nat.card G = nm is at least (2m)m = 2mm.

The generic bound m*(m+1) applies to finite commutative additive carriers, whereas this stronger bound uses cyclicity. Both concern the original Coordinate and its complete nonempty zero-support family exactly equal to the original triples; attaining m-1 graph components alone does not provide these hypotheses. The prior explicit cyclic construction has m*(6*m-7) elements. These bounds do not determine the exact cyclic minimum for general m or the optimal constant in that construction.

An equality example at m = 2 uses ZMod 8 with labels q = 4, p = 1 and a_0 = b_0 = 2. Its eight-element carrier has size 222. An equality example at m = 3 uses ZMod 18 with labels q = 12, p = 5, a_0 = b_0 = 3, a_1 = 4 and b_1 = 2. Its eighteen-element carrier has size 233. At m = 4, ZMod 32 with q = 8, p = 3 and ordered pairs (a_i,b_i) = (1,23), (2,22), (12,12) attains 244 = 32. At m = 5, ZMod 70 with q = 14, p = 48 and ordered pairs (1,55), (9,47), (17,39), (63,63) supplies an upper witness of size 70, above the lower bound 255 = 50. In all four examples, the q label has additive order exactly m, the complete nonempty zero supports are precisely the original triples, and the labeling is noninjective. Equality holds at m = 2, 3 and 4; these examples alone do not establish equality for every m. The parameter-five cyclic minimum is seventy: its lower bound is proved by OriginalCyclicFiveCarrierLowerBound.cyclic_five_carrier_card_lower_bound, and the displayed ZMod 70 realization supplies its upper bound.

Theorem 1.3 (At least m(2*m+1) elements are necessary for an odd carrier).*

Lean statement: D5/S3/Combinatorics/Sequenceability/OriginalSharpnessCarrierLowerBound.odd_carrier_card_lower_bound

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/OriginalSharpnessCarrierLowerBound.odd_carrier_card_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let G be any finite commutative additive group of odd cardinality, let m be a natural number at least two, and let f label the original Coordinate m in G. Write J = Fin(m-1), with distinguished coordinates q,p and paired coordinates a_i,b_i for i in J. Assume addOrderOf(f(q)) = m and the complete coefficient-one zero-support classification: for every finite set C of original coordinates, C is nonempty and its labels sum to zero if and only if C is exactly {q,a_i,b_i} for some i in J. Then m*(2*m+1) is at most Nat.card G. The theorem requires neither cyclicity nor label injectivity.

Put Q = f(q), P = f(p), A_i = f(a_i), H = the additive subgroup generated by Q, and K = G/H. The exact order of Q gives Nat.card H = m. The subgroup-index identity Nat.card G = Nat.card K * Nat.card H implies that Nat.card K is odd, since an odd product has odd factors.

The original support classification separates the classes 0, P and all A_i. Completing a putative subgroup relation with whole a_j,b_j pairs and, when needed, q also excludes P = -A_i and A_i = -A_j for distinct indices. These are the same forbidden-support completions used for the generic and cyclic bounds; a support containing p cannot be prescribed, and the remaining completions violate the exact triple classification.

An odd finite quotient has no nonzero class fixed by negation. Indeed, x = -x implies 2x = 0, so its additive order divides two. A nonzero such class would have order two, forcing two to divide Nat.card K, contrary to oddness. Since every A_i is nonzero, this also excludes A_i = -A_i. Consequently the signed A-classes are all distinct, and the set {0,P} union {A_i,-A_i : i in J} has exactly 2+2(m-1) = 2*m elements.

Thus Nat.card K is at least 2m. Its odd parity improves this to Nat.card K at least 2m+1. Multiplying by the subgroup cardinality m in Nat.card G = Nat.card K * m proves m*(2*m+1) at most Nat.card G. This argument applies to arbitrary finite commutative additive groups of odd cardinality, including m = 2 under the stated hypotheses.

Equality at m = 3 is realized in ZMod 21 with labels q = 7, p = 3, a_0 = 1, b_0 = 13, a_1 = 2 and b_1 = 12. The q label has additive order three, and among all sixty-four subsets of the original six coordinates the only nonempty zero supports are {q,a_0,b_0} and {q,a_1,b_1}. This odd carrier has 21 = 3*(2*3+1) elements, attaining the bound at this parameter. No equality statement for all m is asserted.

References