Three transversals of the H family

Abstract

For every integer K at least nine, under the Latinness premise for the literal H square, the three displayed profiles are transversals. Every two transversals meet, although no entry belongs to all transversals.

Theorem 1.1 (The complete H-family theorem).

$$\forall K\in \mathrm{Int},9\le K\Rightarrow \left(\mathrm{IsLatin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right),\mathrm{square}\left(\mathrm{toNat}\left(K\right)\right)\right)\Rightarrow \left(\mathrm{intCast}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right)=4\cdot K\wedge \left(\left(\forall j\in \mathrm{Fin}\left(3\right),\left(\mathrm{Bijective}\left(\mathrm{column}\left(\mathrm{toNat}\left(K\right),j\right)\right)\wedge \mathrm{Bijective}\left(\mathrm{symbol}\left(\mathrm{toNat}\left(K\right),j\right)\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{symbol}\left(\mathrm{toNat}\left(K\right),j,a\right)=\mathrm{square}\left(\mathrm{toNat}\left(K\right),a,\mathrm{column}\left(\mathrm{toNat}\left(K\right),j,a\right)\right)\right)\wedge \left(\mathrm{IsTransversal}\left(\mathrm{toNat}\left(K\right),T\left(\mathrm{toNat}\left(K\right),j\right)\right)\wedge \mathrm{inter}\left(T\left(\mathrm{toNat}\left(K\right),j\right),D\left(\mathrm{toNat}\left(K\right)\right)\right)=\mathrm{diff}\left(D\left(\mathrm{toNat}\left(K\right)\right),\left\{\mathrm{distinguished}\left(\mathrm{toNat}\left(K\right),j\right)\right\}\right)\right)\right)\right)\wedge \left(\mathrm{inter}\left(T\left(\mathrm{toNat}\left(K\right),0\right),T\left(\mathrm{toNat}\left(K\right),1\right)\right)=\left\{d2\left(\mathrm{toNat}\left(K\right)\right)\right\}\wedge \left(\mathrm{inter}\left(\mathrm{inter}\left(T\left(\mathrm{toNat}\left(K\right),0\right),T\left(\mathrm{toNat}\left(K\right),1\right)\right),T\left(\mathrm{toNat}\left(K\right),2\right)\right)=\left\{\right\}\wedge \left(\left(\forall S\in \mathrm{Set}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right)\right)\right)\right),\forall U\in \mathrm{Set}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right)\right)\right)\right),\mathrm{IsTransversal}\left(\mathrm{toNat}\left(K\right),S\right)\Rightarrow \left(\mathrm{IsTransversal}\left(\mathrm{toNat}\left(K\right),U\right)\Rightarrow \left(\exists e\in \mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right)\right)\right),e\in S\wedge e\in U\right)\right)\right)\wedge \left(\forall e\in \mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right),\mathrm{Fin}\left(\mathrm{order}\left(\mathrm{toNat}\left(K\right)\right)\right)\right)\right),\neg \mathrm{IsPinned}\left(\mathrm{toNat}\left(K\right),e\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Latin/LatinHFamilyTheorem.result (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Afsane Ghafari, Ian M. Wanless (2026). Latin Squares whose transversals intersect in unusual ways. DOI: 10.48550/arXiv.2607.17547. URL: https://arxiv.org/abs/2607.17547v1.

Commentary.

The parameter is an integer at least nine; its natural representative has exactly the same value and gives order four k. Latinness of the actual square is the explicit cited premise. Each literal profile gives one source entry in every row, column and symbol, contains precisely the two distinguished entries indexed by the other profiles, and the first two profiles meet exactly at the third distinguished entry. Their triple intersection is empty. Every arbitrary transversal contains at least two of the three distinguished entries, so any two transversals meet. The three explicit witnesses rule out every pinned entry.

References

• Truth anchor: D5/S3/Combinatorics/Latin/LatinHFamilyTheorem.result
• Dependency: D5/S3/Combinatorics/Latin/LatinHTransversals