Collinear Triple Translation Orbits

Abstract

Translation orbits prove the square-divisibility conjecture in OEIS A146557.

Peter Bala’s July 24, 2025 conjecture concerns unordered triples of points modulo n. No two points may have the same first coordinate or the same second coordinate. Collinearity means the difference determinant vanishes modulo n, including when n is composite.

Definition 1.1 (The square grid).

$$\mathrm{Point}\left(n\right)=\mathrm{ZMod}\left(n\right)\times \mathrm{ZMod}\left(n\right)$$

Formalization. D5/S3/Factorization/CollinearTripleTranslationOrbits.Point (✓ std3).

Citation. OEIS Foundation Inc.; Peter Bala; Max Alekseyev (2025). OEIS A146557 collinear triple divisibility conjecture. URL: https://oeis.org/A146557.

Commentary.

Both coordinates lie in the ring of integers modulo n.

Definition 1.2 (Admissible three-element sets).

$$\begin{array}{r}\mathrm{IsCollinearTriple}\left(S\right)⟺\mathrm{card}\left(S\right)=3\wedge \\ \mathrm{InjOn}\left(fst,S\right)\wedge \mathrm{InjOn}\left(snd,S\right)\wedge \\ \forall p,q,r\in S,(q_1-p_1)(r_2-p_2)=(r_1-p_1)(q_2-p_2)\end{array}$$

Formalization. D5/S3/Factorization/CollinearTripleTranslationOrbits.IsCollinearTriple (✓ std3).

Citation. OEIS Foundation Inc.; Peter Bala; Max Alekseyev (2025). OEIS A146557 collinear triple divisibility conjecture. URL: https://oeis.org/A146557.

Commentary.

The two coordinate projections are injective on S. The determinant identity is required for every p, q, r in S; repeated points satisfy it automatically, and permuting distinct points preserves its vanishing.

Definition 1.3 (The objects being counted).

$$\mathrm{Triple}\left(n\right)=\{S\in \mathrm{Finset}\left(\mathrm{Point}\left(n\right)\right)\mid \mathrm{IsCollinearTriple}\left(S\right)\}$$

Formalization. D5/S3/Factorization/CollinearTripleTranslationOrbits.Triple (✓ std3).

Citation. OEIS Foundation Inc.; Peter Bala; Max Alekseyev (2025). OEIS A146557 collinear triple divisibility conjecture. URL: https://oeis.org/A146557.

Commentary.

An object is a finite set, not an ordered tuple. Its cardinal condition is exactly three, so each unordered configuration contributes once.

Theorem 1.4 (Every fixing translation is three-torsion).

$$\forall n\in \mathbb{N},\forall S\in \mathrm{Triple}\left(n\right),\forall t\in \mathrm{Point}\left(n\right),t+S=S⟹3t=0$$

Proof. Machine-checked in Lean as D5/S3/Factorization/CollinearTripleTranslationOrbits.stabilizing_translation_three_torsion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Summing the three elements of an invariant unordered set gives three times the translation vector plus the original sum. Cancellation forces that vector to be annihilated by three, for every modulus, including modulus zero.

Theorem 1.5 (The A146557 divisibility conjecture).

$$\forall n\in \mathbb{N},0<n⟹\neg (3\mid n)⟹n^2\mid \mathrm{card}\left(\mathrm{Triple}\left(n\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/CollinearTripleTranslationOrbits.square_dvd_card_collinear_triples (✓ std3). ∎

Resolves. Problems/oeis-a146557-collinear-triple-divisibility (proved) by D5/S3/Factorization/CollinearTripleTranslationOrbits.square_dvd_card_collinear_triples.

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc.; Peter Bala; Max Alekseyev (2025). OEIS A146557 collinear triple divisibility conjecture. URL: https://oeis.org/A146557.

Commentary.

Translation preserves coordinate injectivity and every coordinate difference, so it acts on these sets. If translation by t fixes S, summing its three elements before and after translation gives sum(S)=3t+sum(S), hence 3t=0. Since 3 is coprime to n, it is a unit modulo n, and both coordinates of t are zero. The action is therefore free. The standard free-action equivalence identifies the set of configurations with its orbit quotient times the translation group. The latter has n squared elements, proving the divisibility for every positive n not divisible by three.

References

• Truth anchor: D5/S3/Factorization/CollinearTripleTranslationOrbits.IsCollinearTriple
• Truth anchor: D5/S3/Factorization/CollinearTripleTranslationOrbits.Point
• Truth anchor: D5/S3/Factorization/CollinearTripleTranslationOrbits.Triple
• Truth anchor: D5/S3/Factorization/CollinearTripleTranslationOrbits.square_dvd_card_collinear_triples
• Truth anchor: D5/S3/Factorization/CollinearTripleTranslationOrbits.stabilizing_translation_three_torsion