Full technical article: a verified tableau injection
The full technical article From a Failed Corner Slide to a Verified Tableau Injection is now available as an illustrated, 11-page PDF.
Read or download the full article (PDF)
It presents a constructive positivity proof in height two, exact obstructions to earlier proposed constructions, and a Lean-checked coloring formula for every finite alphabet, including the empty palette.
The mathematical theorem and tableau injection were already established by Soojin Cho and JiSun Huh. Our contribution here is their formalization in Lean and an explicit account of the proof and its scope. This is not a new solution of an unsolved mathematical problem.
For an accessible visual introduction, read The beauty of cancellation, with diagrams, social images and a short silent film.
- Final Lean theorem and complete proof repository
- Source-bound verification record
- LaTeX article source
- PDF metadata and SHA-256 checksum
- Cho–Huh’s paper, Section 3.1 and Theorem 3.3
Christopher Yamba · Yamba AI Math. Author-published technical article; not externally peer reviewed.