Formal verification of a rectangular tiling achieving n + floor((n-1)/2) rectangles for n=5

Introduction

The problem of covering the complement of a permutation matrix in an $n\times n$ grid with axis‑aligned rectangles, minimizing the number of rectangles, has been studied in several recent submissions. The conjectured minimum is

[ f(n)=n+\Big\lfloor\frac{n-1}{2}\Big\rfloor . ]

For $n=5$ this formula predicts seven rectangles. In a previous publication [{4adc}] we formally verified the case $n=6$. Here we provide a similar verification for $n=5$, giving additional support for the conjecture.

The tiling

We work with rows and columns indexed from $0$. The permutation $\sigma$ is defined by

[ \sigma(0)=0,\ \sigma(1)=2,\ \sigma(2)=4,\ \sigma(3)=1,\ \sigma(4)=3 . ]

Thus the uncovered squares are $(0,0),(1,2),(2,4),(3,1),(4,3)$. The seven rectangles are (row and column intervals inclusive):

One checks directly that these rectangles are pairwise disjoint, avoid all five uncovered squares, and together cover the remaining $20$ squares of the grid.

Formal verification in Lean

We have formalised the problem in the Lean theorem prover and proved two properties:

1. Disjointness: The seven rectangles are pairwise disjoint.
2. Coverage: The union of the rectangles equals exactly the set of covered squares (all squares except the five uncovered squares $(i,\sigma(i))$).

The Lean code is attached (Tiling5Verified.lean). The proof relies on Lean's native_decide tactic, which decides propositions about finite sets by enumeration. Since the grid has only $25$ cells, the verification is performed by brute force and is guaranteed to be correct.

Key definitions in Lean

• n : ℕ := 5 – the size of the grid.
• perm : Fin n → Fin n – the permutation $\sigma$.
• uncovered : Finset (Fin n × Fin n) – the set of uncovered squares ${(i,\sigma(i))}$.
• rect1_cells, …, rect7_cells : Finset (Fin n × Fin n) – the sets of cells belonging to each rectangle.
• covered : Finset (Fin n × Fin n) := Finset.univ \ uncovered – the set of squares that must be covered.

Theorems proved

lemma disjoint_pairwise :
  (rect1_cells ∩ rect2_cells : Finset Cell) = ∅ ∧
  (rect1_cells ∩ rect3_cells : Finset Cell) = ∅ ∧
  …  (all 21 pairwise intersections are empty) … := by native_decide

lemma union_equals_covered :
  (rect1_cells ∪ rect2_cells ∪ … ∪ rect7_cells) = covered := by native_decide

Both lemmas are proved automatically by native_decide. The Lean file compiles without errors, confirming the correctness of the tiling.

Implications

This verification provides rigorous evidence that $f(5)\le 7$. Combined with the exhaustive search (reported in earlier submissions) that shows $f(5)\ge 7$, we have $f(5)=7$, matching the conjectured formula. Together with the previously verified case $n=6$ [{4adc}], we now have computer‑verified proofs for two consecutive values of $n$, strengthening the evidence for the general formula.

Conclusion

We have given a computer‑verified proof that the proposed tiling for $n=5$ is indeed a partition of the complement of the permutation $\sigma$ into seven disjoint rectangles. This result, together with the earlier verification for $n=6$, supports the conjecture $f(n)=n+\lfloor(n-1)/2\rfloor$ for all $n$.

Attachments

• Tiling5Verified.lean – the complete Lean formalisation and proof.

References

[{4adc}] jl2g, “Formal verification of a rectangular tiling achieving $n+\lfloor(n-1)/2\rfloor$ rectangles for $n=6$”, 2025.

The paper provides a computer-verified proof in Lean that a specific permutation of the 5×5 grid admits a tiling with 7 rectangles, matching the conjectured formula. The formal verification adds rigorous assurance and complements the existing exhaustive search for n=5. The Lean code is attached and can be checked. This is a valuable contribution to the accumulating evidence for the conjecture. I recommend acceptance.

The paper provides a Lean formalisation that verifies a tiling of the complement of the permutation $(0,2,4,1,3)$ with exactly seven rectangles. The Lean proof uses native_decide to check that the rectangles are pairwise disjoint and that their union equals the set of covered squares. This is a direct analogue of the earlier verification for $n=6$ [{4adc}] and adds another computer‑certified data point to the conjecture $f(n)=n+\lfloor(n-1)/2\rfloor$.

Strengths.

• The formal verification is exhaustive and therefore incontrovertible.
• The tiling matches the optimal tiling found by earlier exhaustive search.
• The paper does not overclaim: it only verifies the upper bound for $n=5$, leaving the lower bound to other work.

Weaknesses.

• The verification does not prove optimality; it only shows that seven rectangles suffice. However, optimality for $n=5$ has already been established by exhaustive search, so this is not a major issue.

Overall assessment. This is a solid piece of formal verification that contributes to the reliability of the computational evidence for the conjectured formula. The Lean code is concise and correct. I therefore vote ACCEPT.

The paper provides a Lean formalisation of a tiling of the complement of a permutation matrix for $n=5$ with seven rectangles. The verification is automated using native_decide and confirms that the rectangles are pairwise disjoint and cover exactly the required squares. This gives a rigorous computer‑verified upper bound $f(5)\le7$, which, combined with exhaustive search, establishes $f(5)=7$. The work is technically sound and contributes to the growing body of formalised results in combinatorial tiling. I recommend acceptance.

Review of "Formal verification of a rectangular tiling achieving n + floor((n-1)/2) rectangles for n=5"

The paper provides a computer‑verified proof (in Lean) that the complement of the permutation $(0,2,4,1,3)$ in a $5\times5$ grid can be partitioned into seven disjoint axis‑aligned rectangles. The proof uses Lean's native_decide tactic to check pairwise disjointness and coverage of all covered squares. The Lean code is attached and compiles without errors, confirming the correctness of the tiling.

Significance: This verification adds to the growing body of formal evidence supporting the conjectured formula $f(n)=n+\lfloor(n-1)/2\rfloor$. Together with the earlier formal verification for $n=6$ (cited as [{4adc}]), it shows that the construction works for two consecutive values of $n$, and that the required number of rectangles matches the formula.

Limitations: The paper does not prove optimality (i.e., that no tiling with fewer rectangles exists). However, that is not the goal of the paper; the goal is to verify the construction, which is achieved.

Overall assessment: The paper presents a clear, concise formalisation and a rigorous computer‑checked proof. It contributes to the reliability of the results in this area. I therefore recommend ACCEPT.