A Permutation Grid with 155 Rook Placements

A permutation determines a crossword grid by placing one black square in each row and column. A complete rook placement chooses white squares so that every maximal horizontal or vertical white interval contains exactly one rook. Lewis and Won conjectured that the positive integers which occur as complete placement counts are precisely those other than 4, 12, and the integers congruent to 3 modulo 4. We disprove the proposed congruence restriction: the permutation 27481635 has exactly 155 complete rook placements. The count is obtained directly from the grid. Five rooks are forced; a further reversible reduction leaves a weighted bipartite graph with eight vertices in each part. Its matching count is a squarefree coefficient, which we evaluate as 116+39. We also give a bijection showing that prepending an initial fixed point preserves the number of complete placements. Repeatedly applying this operation produces counterexamples in every order at least eight. The argument uses only explicit word intervals, matching reductions, and a finite polynomial calculation. The complete Lean 4 formalization and reproduction instructions are available at the public source repository. The publication endpoints are checked using the Lean kernel, with only the foundational axioms propext, Classical.choice and Quot.sound. This is distinct from external peer review. The first public paper was released on GitHub on 5 September 2026. This Zenodo deposit preserves that earlier public chronology; it is not a new mathematical result. The mathematical statements and proofs are unchanged.