Lean 4 ನಲ್ಲಿ Collatz Exit-Layer Convergence ನ ಔಪಚಾರಿಕೀಕರಣ

ನಾನು Lean 4 ನಲ್ಲಿ ಹೊಸ ವಿಧಾನಾತ್ಮಕ ದಾಖಲೆಯನ್ನು (methodological record) ಹಂಚಿಕೊಳ್ಳುತ್ತಿದ್ದೇನೆ.

ಈ ಕೆಲಸವು Collatz ಡೈನಾಮಿಕ್ಸ್‌ನ ಒಂದು ನಿರ್ದಿಷ್ಟ ಭಾಗವನ್ನು ಔಪಚಾರಿಕೀಕರಿಸುತ್ತದೆ. ಇದನ್ನು ನಾವು exit-layer fragment ಎಂದು ಕರೆಯುತ್ತೇವೆ. ಇದು ಒಂದು ಹಂತದಲ್ಲಿ power-of-two ಗೆ ತಲುಪುವ ಬೆಸ ಸಂಖ್ಯೆಗಳನ್ನು ಒಳಗೊಂಡಿದೆ.

ಇದು ಸಂಪೂರ್ಣ Collatz conjecture ನ ಪುರಾವೆಯಲ್ಲ. ಇದು ತಿಳಿದಿರುವ ಗಣಿತೀಯ ಅವಲೋಕನದ ಒಂದು ಔಪಚಾರಿಕ ದಾಖಲೆಯಾಗಿದೆ.

ಪ್ರಮುಖ ತಾಂತ್ರಿಕ ವಿವರಗಳು:

• ನಾವು orbits ಅನ್ನು ಪ್ರತಿನಿಧಿಸಲು coinductive Stream' coalgebras ಅನ್ನು ಬಳಸುತ್ತೇವೆ. • ನಾವು Collatz ಹಂತದ halt-at-1 variant ಅನ್ನು ವ್ಯಾಖ್ಯಾನಿಸುತ್ತೇವೆ. • ಇದು orbit ಅನ್ನು ಅಂತಿಮವಾಗಿ 1 ರಲ್ಲಿ ಸ್ಥಿರವಾಗುವಂತೆ ಮಾಡುತ್ತದೆ. • exit-layer ಸಂಖ್ಯೆಗಳು ಈ ಸ್ಥಿರ ಸ್ಟ್ರೀಮ್‌ಗೆ (constant stream) ತಲುಪುತ್ತವೆ ಎಂದು ನಾವು ಸಾಬೀತುಪಡಿಸುತ್ತೇವೆ. • ಈ ಪುರಾವೆಯು ಪ್ರಮಾಣಿತ Mathlib axiom triple ಮೇಲೆ ಅವಲಂಬಿತವಾಗಿದೆ.

ಒಂದು ಗಮನಾರ್ಹ ಫಲಿತಾಂಶ:

head_collatzOrbit ಎಂಬ ಪ್ರಮೇಯವು ಸಂಪೂರ್ಣವಾಗಿ axiom-free ಆಗಿದೆ. ಈ ಪ್ರಮೇಯದ ಮೇಲೆ #print axioms ಅನ್ನು ರನ್ ಮಾಡಿದರೆ ಖಾಲಿ ಸೆಟ್ (empty set) ಸಿಗುತ್ತದೆ. ಇದು ಇದನ್ನು ಪ್ರಮಾಣಿತ ಶಾಸ್ತ್ರೀಯ axiom base ಗಿಂತ ಕೆಳಗಿನ ಮಟ್ಟದಲ್ಲಿ ಇರಿಸುತ್ತದೆ.

ಈ ಪ್ರಬಂಧವು ಮಾಡದಿದ್ದವುಗಳು:

ನಮ್ಮ ಅವಲೋಕಿತ ವ್ಯಾಪ್ತಿಯೊಳಗೆ ಸ್ವಚ್ಛವಾದ, axiom-free ಔಪಚಾರಿಕೀಕರಣವನ್ನು ಒದಗಿಸುವುದು ಇದರ ಗುರಿಯಾಗಿದೆ. ನಾವು Kim (2008) ರ coalgebraic ದೃಷ್ಟಿಕೋನವನ್ನು ಬಳಸುತ್ತೇವೆ ಮತ್ತು ಅದನ್ನು Lean 4 ಗೆ ಅನ್ವಯಿಸುತ್ತೇವೆ.

ಇದು Rei-AIOS ಸರಣಿಗೆ ಒಂದು ವಿಧಾನಾತ್ಮಕ ಕೊಡುಗೆಯಾಗಿದೆ. ಇದು axiom-base ಕನಿಷ್ಠೀಕರಣ ಮತ್ತು ತಿಳಿದಿರುವ ರಚನೆಗಳನ್ನು ಔಪಚಾರಿಕೀಕರಿಸುವತ್ತ ಗಮನಹರಿಸುತ್ತದೆ.

ಮೂಲ: 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