Lean 4 ਵਿੱਚ Collatz Exit-Layer Convergence ਦਾ Formalization
ਮੈਂ Lean 4 ਵਿੱਚ ਇੱਕ ਨਵਾਂ ਵਿਧੀਗਤ ਰਿਕਾਰਡ (methodological record) ਸਾਂਝਾ ਕਰ ਰਿਹਾ ਹਾਂ।
ਇਹ ਕੰਮ Collatz dynamics ਦੇ ਇੱਕ ਖਾਸ ਹਿੱਸੇ ਨੂੰ formalize ਕਰਦਾ ਹੈ। ਅਸੀਂ ਇਸਨੂੰ exit-layer fragment ਕਹਿੰਦੇ ਹਾਂ। ਇਹ ਉਹਨਾਂ ਟਾਂਕ ਸੰਖਿਆਵਾਂ (odd numbers) ਨੂੰ ਕਵਰ ਕਰਦਾ ਹੈ ਜੋ ਇੱਕ ਕਦਮ ਵਿੱਚ power-of-two ਤੱਕ ਪਹੁੰਚ ਜਾਂਦੀਆਂ ਹਨ।
ਇਹ ਪੂਰੇ Collatz conjecture ਦਾ ਸਬੂਤ ਨਹੀਂ ਹੈ। ਇਹ ਇੱਕ ਜਾਣੇ-ਪਛਾਣੇ ਗਣਿਤਕ ਨਿਰੀਖਣ (mathematical observation) ਦਾ ਇੱਕ formal ਰਿਕਾਰਡ ਹੈ।
ਮੁੱਖ ਤਕਨੀਕੀ ਵੇਰਵੇ:
• ਅਸੀਂ orbits ਨੂੰ ਦਰਸਾਉਣ ਲਈ coinductive Stream' coalgebras ਦੀ ਵਰਤੋਂ ਕਰਦੇ ਹਾਂ। • ਅਸੀਂ Collatz step ਦਾ ਇੱਕ halt-at-1 variant ਪਰਿਭਾਸ਼ਿਤ ਕਰਦੇ ਹਾਂ। • ਇਹ orbit ਨੂੰ ਅੰਤ ਵਿੱਚ 1 'ਤੇ ਸਥਿਰ (constant) ਬਣਾ ਦਿੰਦਾ ਹੈ। • ਅਸੀਂ ਸਾਬਤ ਕਰਦੇ ਹਾਂ ਕਿ exit-layer ਸੰਖਿਆਵਾਂ ਇਸ constant stream ਤੱਕ ਪਹੁੰਚਦੀਆਂ ਹਨ। • ਇਹ ਸਬੂਤ ਮਿਆਰੀ Mathlib axiom triple 'ਤੇ ਨਿਰਭਰ ਕਰਦਾ ਹੈ।
ਇੱਕ ਮਹੱਤਵਪੂਰਨ ਨਤੀਜਾ:
ਥਿਊਰਮ head_collatzOrbit ਪੂਰੀ ਤਰ੍ਹਾਂ axiom-free ਹੈ। ਇਸ ਥਿਊਰਮ 'ਤੇ #print axioms ਚਲਾਉਣ ਨਾਲ ਇੱਕ ਖਾਲੀ ਸੈੱਟ (empty set) ਮਿਲਦਾ ਹੈ। ਇਹ ਇਸਨੂੰ ਮਿਆਰੀ ਕਲਾਸੀਕਲ axiom base ਤੋਂ ਵੀ ਹੇਠਾਂ ਰੱਖਦਾ ਹੈ।
ਇਹ ਪੇਪਰ ਕੀ ਨਹੀਂ ਕਰਦਾ:
- ਇਹ Collatz conjecture ਨੂੰ ਹੱਲ ਨਹੀਂ ਕਰਦਾ।
- ਇਹ Cases 5–8 trailing-1-bits ਦੀ ਕੰਧ ਨੂੰ ਨਹੀਂ ਤੋੜਦਾ।
- ਇਹ Terence Tao ਦੇ ਵਿਸ਼ਲੇਸ਼ਣਾਤਮਕ (analytic) ਨਤੀਜਿਆਂ ਨੂੰ ਨਹੀਂ ਬਦਲਦਾ।
- ਇਹ Janik (2026) ਦੇ ਅਣਸੁਲਝੇ ਹਿੱਸਿਆਂ ਨੂੰ ਹੱਲ ਨਹੀਂ ਕਰਦਾ।
ਇਸਦਾ ਉਦੇਸ਼ ਸਾਡੀ ਦੇਖੀ ਗਈ ਸੀਮਾ (observed range) ਦੇ ਅੰਦਰ ਇੱਕ ਸਾਫ਼, axiom-free formalization ਪ੍ਰਦਾਨ ਕਰਨਾ ਹੈ। ਅਸੀਂ Kim (2008) ਦੇ coalgebraic ਦ੍ਰਿਸ਼ਟੀਕੋਣ ਦੀ ਵਰਤੋਂ ਕਰਦੇ ਹਾਂ ਅਤੇ ਇਸਨੂੰ Lean 4 'ਤੇ ਲਾਗੂ ਕਰਦੇ ਹਾਂ।
ਇਹ Rei-AIOS ਸੀਰੀਜ਼ ਵਿੱਚ ਇੱਕ ਵਿਧੀਗਤ ਯੋਗਦਾਨ ਹੈ। ਇਹ axiom-base ਘਟਾਉਣ (minimization) ਅਤੇ ਜਾਣੇ-ਪਛਾਣੇ ਢਾਂਚਿਆਂ (structures) ਨੂੰ formalize ਕਰਨ 'ਤੇ ਕੇਂਦਰਿਤ ਹੈ।
ਵਿਕਲਪਿਕ ਲਰਨਿੰਗ ਕਮਿਊਨਿਟੀ: https://t.me/GyaanSetuAi