Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Translated quotient bounds

Abstract

A translated signed-label set gives quadratic bounds for cyclic and odd-order original-support carriers.

In both results, G is a finite abelian group, m is at least three, and f labels the entire original Coordinate m. The distinguished q label has additive order exactly m. For every finite coordinate subset C, nonemptiness together with a zero label sum is equivalent to C being exactly the original triple {q,a_i,b_i} for some pair index i. These are the full original hypotheses; label separation and signed-triple exclusion are derived from them.

Theorem 1.1 (A cyclic carrier has at least 4m(m-2) elements).

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

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

Source. Repository-derived.

Commentary.

If G is cyclic, its cardinality is at least 4m(m-2). This is a uniform lower bound, without an assertion of optimality. Combining this bound with the existing signed construction at k=one, for every odd m at least three the least cardinality of a cyclic carrier satisfying the same complete original hypotheses lies between 4m(m-2) and 4m(m-1), a pointwise interval of width 4m with common quadratic term 4m^2.

For m at least four, pass to K=G/<f(q)> and let A_i be the quotient class of f(a_i). Put r=m-1 and T={0} union {A_i,-A_i}. The existing original-support lemmas make A_i nonzero and place distinct indices in distinct negation orbits. The full all-signs triple lemma excludes a zero sum of three signed labels at distinct indices. The quotient is cyclic, so the zero fiber of doubling has at most two elements, and every doubling fiber injects into it by translation.

For any selected a=A_o, a collision x in T intersect (a+T) lies in {0,a,-a,2a} or satisfies 2x=a. If neither signed label is zero, a repeated selected index gives one of the four explicit exceptions; equal pair indices give either a=zero, which is impossible, or the retained doubling equation. Three distinct indices give the forbidden signed triple. Thus no sign choice or root-fiber exception is omitted.

If no selected A_i is self-negative, T has 2r+1 elements and its translated intersection has at most six elements. If a selected nonzero h is self-negative, the overlap of the positive and negative label sets has at most one element, so T has at least 2r elements. Choosing a=h reduces the four explicit exceptions to {0,h}; the intersection then has at most four elements. In both cases, inclusion-exclusion gives card(K) at least 4*r-4. The subgroup generated by f(q) has exactly m elements, giving the stated bound. At m=three, the existing cyclic lower bound supplies the boundary case.

Theorem 1.2 (An odd-order abelian carrier has at least m(4*m-7) elements).*

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

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

Source. Repository-derived.

Commentary.

If card(G) is odd, its cardinality is at least m*(4*m-7). No cyclicity hypothesis is needed, and no optimality assertion is made.

The same quotient K has odd cardinality. Its zero doubling fiber consists only of zero: the additive order of a point killed by two divides both two and the odd group cardinality. Every doubling fiber therefore has at most one element, and no selected nonzero A_i is self-negative. The same complete collision list gives card(T)=2r+1 and translated intersection cardinality at most five. Inclusion-exclusion gives card(K) at least 4r-3, and multiplication by the exact m-element subgroup gives card(G) at least m*(4*m-7). At m=three, the previously established odd-order bound supplies the boundary case.

References