Formalizing building-up constructions of self-dual codes through isotropic lines in Lean
यह शोधपत्र बाइनरी सेल्फ-डुअल कोड्स के किम (Kim) और चिनबर्ग-झांग (Chinburg-Zhang) के निर्माणों के बीच तुल्यता स्थापित करता है, बीजगणितीय और ज्यामितीय दृष्टिकोणों को एकीकृत करने के लिए $-1q \equiv 1 \pmod{4}q$-ary क्षेत्रों तक विस्तारित करता है, और विभिन्न इष्टतम एवं MDS सेल्फ-डुअल कोड्स को कुशलतापूर्वक निर्मित करने के लिए इन परिणामों का लीन 4 (Lean 4) औपचारिक रूप प्रदान करता है।