Suirodoku: A Graeco-Latin Sudoku Square — CSP Formalization, Bijection Theorem, and the God Digit Problem

We introduce Suirodoku, a 9×9 combinatorial puzzle combining Sudoku constraints with Graeco-Latin square orthogonality. Each cell contains an ordered pair (digit, color) where both projections satisfy Sudoku constraints, and each pair appears exactly once. We establish existence constructively, provide a complete CSP formalization within Berthier's Multi-Sorted First Order Logic framework, comprising a Grid Theory (six sorts with exhaustivity axioms), a Suirodoku Theory (ten constraint axioms including a global pair uniqueness axiom), and instance-specific puzzle axioms. We prove a Bijection Theorem conferring absolute identity to each cell — a property absent from classical Sudoku. We derive solving heuristics (Rainbow and Chromatic Circle techniques), and pose the God Digit Problem: must every uniquely solvable Suirodoku puzzle contain all 9 digits among its clues? We prove a Dichotomy Theorem showing that either no symbol is critical, or all symbols are critical.