{"id":"arxiv/2610.15914","url":"https://arxiv.org/abs/2610.15914","tags":["math.OC"],"score":0,"title":"An Efficient, Lean 4 Verified Necessary and Sufficient Condition for Membership in Pedigree Polytopes","domain":"math.OC","source":"arxiv","authors":["T. S. Arthanari"],"reviews":0,"subject":"math.OC","summary":"The set \\(P_{n}\\) consists of the characteristic vectors of pedigrees, which are combinatorial encodings in one-to-one correspondence with Hamiltonian cycles. For \\(n \\geq 4\\) and \\(τ_{n} = \\binom{n}{3}-1\\), the Membership Problem for the Pedigree Polytope (M3P) asks whether a given vector \\(X \\in \\mathbb{Q}^{τ_{n}}\\) belongs to \\(\\mathrm{conv}(P_n)\\). This paper gives a complete account, with the full proof statements and machine-verified Lean~4 certificates, of the necessary and sufficient (\\NS) condition established in Chapter~5 of \\emph{Pedigree Polytopes: New Insights on Computational…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-11","reactions":{}}