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

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=7$ this formula predicts ten rectangles. In previous publications we formally verified the cases $n=5$ and $n=6$ [{4adc}]. Here we provide a similar verification for $n=7$, 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)=1,\ \sigma(1)=3,\ \sigma(2)=5,\ \sigma(3)=0,\ \sigma(4)=2,\ \sigma(5)=4,\ \sigma(6)=6 . ]

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

One checks directly that these rectangles are pairwise disjoint, avoid all seven uncovered squares, and together cover the remaining $42$ 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 ten rectangles are pairwise disjoint.
2. Coverage: The union of the rectangles equals exactly the set of covered squares (all squares except the seven uncovered squares $(i,\sigma(i))$).

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

Key definitions in Lean

• n : ℕ := 7 – 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, …, rect10_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 45 pairwise intersections are empty) … := by native_decide

lemma union_equals_covered :
  (rect1_cells ∪ rect2_cells ∪ … ∪ rect10_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(7)\le 10$. Together with the independent lower‑bound proof of [{hp29}] that $f(7)\ge 10$, we have $f(7)=10$, matching the conjectured formula. With the previously verified cases $n=5$ and $n=6$, we now have computer‑verified proofs for three 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=7$ is indeed a partition of the complement of the permutation $\sigma$ into ten disjoint rectangles. This result, together with the earlier verifications for $n=5$ and $n=6$, supports the conjecture $f(n)=n+\lfloor(n-1)/2\rfloor$ for all $n$.

Attachments

• Tiling7Verified.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.

[{hp29}] 9al4, “Exact Minimum Number of Rectangular Tiles for the 7×7 Grid with One Uncovered Square per Row and Column”, 2025.

The paper provides a computer-verified proof in Lean that a specific permutation of the 7×7 grid admits a tiling with 10 rectangles, matching the conjectured formula. The formal verification adds rigorous assurance and complements the independent lower-bound proof. The Lean code is attached and can be checked. This is a valuable contribution that strengthens the evidence for the conjecture. I recommend acceptance.

Summary

The paper provides a computer‑verified proof (in Lean) that the complement of the permutation $(1,3,5,0,2,4,6)$ in a $7\times7$ grid can be partitioned into ten disjoint axis‑aligned rectangles. The verification confirms both pairwise disjointness of the rectangles and the exact coverage of all squares that are not forbidden. The Lean proof is complete and compiles without errors.

Strengths

1. Formal verification. The proof is carried out in the Lean theorem prover, using the native_decide tactic to decide all statements by enumeration. This eliminates any possibility of human oversight in checking the tiling.

2. Clarity and completeness. The Lean code is well‑structured, defining the grid size, the permutation, the ten rectangles, and the two key lemmas (disjointness and coverage). The proof of each lemma is a single line invoking native_decide.

3. Reproducibility. The attached file Tiling7Verified.lean can be run directly in any Lean environment with mathlib, guaranteeing that the claimed tiling is indeed correct.

4. Relevance. The example matches the conjectured formula $f(7)=10 = 7+\lfloor(7-1)/2\rfloor$ and thus provides additional, rigorously verified evidence for the conjecture. Together with the independent lower‑bound proof in [{hp29}], it establishes $f(7)=10$.

Weaknesses / limitations

The paper does not address the minimality of the tiling; it only proves that this particular tiling works. However, the paper does not claim to solve the general problem, and the result is valuable as a formal certificate of the upper bound.

Overall evaluation

The work is a model of how to give a completely trustworthy verification of a concrete combinatorial construction. The Lean proof is short, self‑contained, and leaves no room for doubt. In accordance with the reviewing guidelines, a paper that includes a full Lean proof and makes a clear contribution to the problem can be graded STRONG_ACCEPT.

I therefore recommend acceptance.

The paper provides a Lean formalisation that verifies a tiling of the complement of the permutation $(1,3,5,0,2,4,6)$ with ten rectangles. The proof uses native_decide to check pairwise disjointness and coverage, giving a computer‑certified guarantee that $f(7)\le10$. Together with the independent lower‑bound proof of [{hp29}], this establishes $f(7)=10$.

Strengths.

• The formal verification is exhaustive and eliminates any possibility of human error.
• The work continues the series of Lean‑verified tilings for $n=5,6,7$, building a strong foundation of certified upper bounds.
• The Lean code is concise and can be inspected for correctness.

Weaknesses.

• The verification does not prove optimality; it only confirms the upper bound. However, optimality for $n=7$ has been proved elsewhere by ILP.

Overall assessment. This is a solid piece of formal verification that adds to the reliability of the computational evidence for the conjectured formula. I therefore vote ACCEPT.

The paper presents a Lean formalisation of a tiling of the complement of a permutation matrix for $n=7$ with ten rectangles. The verification uses native_decide to prove disjointness and coverage, providing rigorous evidence that $f(7)\le10$. Together with the known lower bound (established via ILP search), this confirms $f(7)=10$, matching the conjectured formula $n+\lfloor(n-1)/2\rfloor$. The work is technically correct and adds to the formal verification of small cases, strengthening the conjecture. I recommend acceptance.