𝗟𝗲𝗮𝗻 𝟰-இல் Collatz exit-layer குவிதலை முறைப்படுத்துதல்

Lean 4-இல் ஒரு புதிய வழிமுறைப் பதிவைப் (methodological record) பகிர்ந்து கொள்கிறேன்.

இந்த ஆய்வு Collatz இயக்கவியலின் (dynamics) ஒரு குறிப்பிட்ட பகுதியை முறைப்படுத்துகிறது. இதை நாங்கள் exit-layer fragment என்று அழைக்கிறோம். இது ஒரு படியிலேயே இரண்டு-ன் அடுக்கிற்கு (power-of-two) வந்து சேரும் ஒற்றை எண்களை உள்ளடக்கியது.

இது முழுமையான Collatz ஊகத்திற்கான (conjecture) நிரூபணம் அல்ல. இது அறியப்பட்ட ஒரு கணித அவதானிப்பின் (mathematical observation) முறையான பதிவு மட்டுமே.

முக்கிய தொழில்நுட்ப விவரங்கள்:

• சுற்றுப்பாதைகளை (orbits) பிரதிநிதித்துவப்படுத்த நாங்கள் coinductive Stream' coalgebras-ஐப் பயன்படுத்துகிறோம். • Collatz படிநிலையின் 'halt-at-1' மாறுபாட்டை (variant) நாங்கள் வரையறுக்கிறோம். • இது சுற்றுப்பாதையை இறுதியில் 1 என்ற நிலையான மதிப்பில் நிறுத்துகிறது. • exit-layer எண்கள் இந்த நிலையான ஓட்டத்தை (constant stream) அடைகின்றன என்பதை நாங்கள் நிரூபிக்கிறோம். • இந்த நிரூபணம் நிலையான Mathlib axiom triple-ஐச் சார்ந்துள்ளது.

ஒரு குறிப்பிடத்தக்க முடிவு:

head_collatzOrbit என்ற தேற்றம் முற்றிலும் தற்கருத்துகளற்றது (axiom-free). இந்தத் தேற்றத்தில் #print axioms என்பதை இயக்கினால் ஒரு வெற்றுத் தொகுப்பு (empty set) கிடைக்கும். இது இதனை நிலையான செவ்வியல் தற்கருத்துத் தளத்திற்கு (standard classical axiom base) கீழும் வைக்கிறது.

இந்த ஆய்வுக் கட்டுரை செய்யாதவை:

எங்கள் அவதானிக்கப்பட்ட வரம்பிற்குள் (observed range), ஒரு தெளிவான, தற்கருத்துகளற்ற (axiom-free) முறைப்படுத்துதலை வழங்குவதே இதன் நோக்கமாகும். நாங்கள் Kim (2008)-இன் coalgebraic கண்ணோட்டத்தைப் பயன்படுத்தி அதை Lean 4-இல் செயல்படுத்துகிறோம்.

இது Rei-AIOS தொடருக்கான ஒரு வழிமுறைப் பங்களிப்பாகும். இது தற்கருத்துத் தளத்தைக் குறைப்பதிலும் (axiom-base minimization) அறியப்பட்ட கட்டமைப்புகளை முறைப்படுத்துவதிலும் கவனம் செலுத்துகிறது.

மூலம்: 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