Independence in Cartesian Cayley squares
Abstract
Independent sets have a per-row upper bound; a difference-set construction attains that bound in finite abelian Cayley squares.
Theorem 1.1 (Counting independent vertices by rows).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Products/CayleyIndependence.card_le_layer_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
In a Cartesian product G □ H with H finite, the second coordinates in each fixed row form an independent set of H. If every selected first coordinate belongs to the finite set R, summing the row bounds gives |I| ≤ |R| alpha(H). The first factor may be infinite; both factors may be empty or disconnected.
Theorem 1.2 (The full abelian square equality).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Products/CayleyIndependence.indepNum_addCayley_square (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let A be any finite additive abelian group, and let S avoid zero and be closed under negation. The native Cayley adjacency is exactly y-x in S. For a maximum independent set B, the pairs (x,x+b), with x in A and b in B, form an independent set in the Cartesian square. Injectivity gives |A||B| vertices and attains the row bound. Connectedness is unnecessary; the trivial group, an empty connection set, and self-inverse steps are included.