← All papers
Correction: N-free posets and orthomodularity
math.CO
Jul 20, 2026 · v1
TL;DR
The corrected theorem and all valid results of the original N-free posets paper are formalized in Lean 4, with a public GitHub repository.
Abstract
We present a corrected version of a theorem from the paper "N-free posets and orthomodularity" published in Order 43(1) (2026).
Problem
A published theorem claimed that a finite poset has a compatible incomparability orthoset if and only if it contains no 'weak N' configuration. A five-element counterexample poset, called the X, shows the claim is false.
Approach
The note defines X and covering-X configurations. It proves that a finite poset contains an X if and only if it contains a covering X. It then proves the corrected equivalence by showing that each forbidden configuration blocks compatibility, and conversely. All results, along with the valid results of the original paper, are formalized in Lean 4.
Results
A finite poset has a compatible incomparability orthoset if and only if it contains no weak N and no X. The Lean 4 formalization is available on GitHub.