Paper 3. Sixteen Cards

Osman, Mohamed A.

Paper 3. Sixteen Cards

A finite reduction to 463 canonical cores, SAT, and independently checked DRAT proofs

Mohamed A. Osman · ORCID 0009-0004-5912-999X · independent researcher · 2026-10-19

Download the PDF · source on GitHub · repository · concept DOI

Abstract. A hypothetical sixteen-card counterexample is reduced to one of 463 canonical eight-card cores; for each core the completion problem is written as a CNF formula; all 463 are unsatisfiable; and each unsatisfiability carries a DRAT certificate accepted by an independent proof checker. DRAT certification removes the SAT solver from the trusted base, but the completeness of the reduction and the faithfulness of the encoding remain separate obligations, stated as open.

No priority is claimed for any result, and this is not presented as a settled answer. The lower bound is computer-assisted and has not been independently reviewed by a human or by a proof assistant. AI tools were used throughout the work and its review; every computational claim is regenerated by a script or certified by a proof file in code/ and results/ of the repository. Licence: CC BY 4.0 (text), MIT (code).