𝗟𝗲𝗮𝗻 𝟰 లో Collatz Exit-Layer Convergence యొక్క ఫార్మలైజేషన్

నేను Lean 4 లో ఒక కొత్త పద్ధతిపరమైన (methodological) రికార్డును పంచుకుంటున్నాను.

ఈ పని Collatz డైనమిక్స్‌లోని ఒక నిర్దిష్ట భాగాన్ని ఫార్మలైజ్ చేస్తుంది. దీనిని మేము exit-layer fragment అని పిలుస్తాము. ఇది ఒకే దశలో power-of-two కి చేరుకునే బేసి సంఖ్యలను (odd numbers) కవర్ చేస్తుంది.

ఇది పూర్తి Collatz conjecture కి నిరూపణ కాదు. ఇది ఒక తెలిసిన గణిత పరిశీలన యొక్క ఫార్మల్ రికార్డు.

ముఖ్యమైన సాంకేతిక వివరాలు:

• ఆర్బిట్‌లను (orbits) సూచించడానికి మేము coinductive Stream' coalgebras ను ఉపయోగిస్తాము. • మేము Collatz స్టెప్ యొక్క 'halt-at-1' వేరియంట్‌ను నిర్వచిస్తాము. • ఇది ఆర్బిట్‌ను చివరికి 1 వద్ద స్థిరంగా (constant) మారుస్తుంది. • exit-layer సంఖ్యలు ఈ స్థిరమైన స్ట్రీమ్‌కు చేరుకుంటాయని మేము నిరూపిస్తాము. • ఈ నిరూపణ ప్రామాణిక Mathlib axiom triple పై ఆధారపడి ఉంటుంది.

ఒక ముఖ్యమైన ఫలితం:

head_collatzOrbit అనే థియరమ్ పూర్తిగా axiom-free. ఈ థియరమ్‌పై #print axioms రన్ చేస్తే ఖాళీ సెట్ (empty set) వస్తుంది. ఇది దీనిని ప్రామాణిక క్లాసికల్ ఆక్సియమ్ బేస్ కంటే దిగువన ఉంచుతుంది.

ఈ పేపర్ ఏమి చేయదు:

మా పరిశీలన పరిధిలో ఒక స్వచ్ఛమైన, axiom-free ఫార్మలైజేషన్‌ను అందించడమే దీని లక్ష్యం. మేము Kim (2008) నుండి coalgebraic దృక్పథాన్ని ఉపయోగించి దానిని Lean 4 కి వర్తింపజేస్తాము.

ఇది Rei-AIOS సిరీస్‌కు ఒక పద్ధతిపరమైన (methodological) సహకారం. ఇది axiom-base కనిష్ఠీకరణ (minimization) మరియు తెలిసిన నిర్మాణాలను ఫార్మలైజ్ చేయడంపై దృష్టి పెడుతుంది.

Source: https://dev.to/fc0web/paper-166-v01-a-lean-4-axiom-free-formalization-of-exit-layer-collatz-convergence-as-a-stream-8oi

ఐచ్ఛిక అభ్యాస సమూహం: https://t.me/GyaanSetuAi