Le verrou ΛS,k en action
The ΛS,k lock in action
Faites varier $S$ et $k$ et observez en direct la valeur du verrou diophantien $\Lambda_{S,k} = S \log 2 - k \log 3$, ainsi que les régions interdites par chacune des trois hypothèses externes (BakerSeparation, BarinaVerification, DerivedLargeKBound).
Vary $S$ and $k$ and observe in real time the value of the Diophantine lock $\Lambda_{S,k} = S \log 2 - k \log 3$, along with the regions forbidden by each of the three external hypotheses (BakerSeparation, BarinaVerification, DerivedLargeKBound).
Pourquoi $\Lambda_{S,k}$ est le verrou central
Why $\Lambda_{S,k}$ is the central lock
Pour qu'un cycle Collatz hypothétique de longueur $k$ existe, il faut que $S \cdot \log 2 \approx k \cdot \log 3$, c'est-à-dire $\Lambda_{S,k} \approx 0$. Mais $\log_2 3$ est irrationnel, donc cette égalité ne peut être qu'approchée. De combien ? C'est ce que mesure une borne effective de type Baker. Notre axiome BakerSeparation utilise la forme $(2^s - 3^k) \cdot k^6 \geq 3^k$ comme conjecture de travail : renforcement non démontré des bornes diophantiennes publiées (Rhin 1987, Salikhov 2007, Wu 2003, Simons-de Weger 2005), pas un théorème externe — voir mea culpa #28 et le lemme δ10 (Phase 64) qui démontre formellement pourquoi aucune borne publiée ne suffit.
For a hypothetical Collatz cycle of length $k$ to exist, we need $S \cdot \log 2 \approx k \cdot \log 3$, i.e. $\Lambda_{S,k} \approx 0$. But $\log_2 3$ is irrational, so this equality can only be approximate. By how much? This is what an effective Baker-type bound measures. Our BakerSeparation axiom uses the form $(2^s - 3^k) \cdot k^6 \geq 3^k$ as a working hypothesis (conjecture): undemonstrated strengthening of published Diophantine bounds (Rhin 1987, Salikhov 2007, Wu 2003, Simons-de Weger 2005), not an external theorem — see mea culpa #28 and the δ10 lemma (Phase 64) which formally proves why no published bound is sufficient.
$n < 2^{71}$ vérifié
$n < 2^{71}$ verified
Couvre les petits cycles ($k \leq 1322$) en combinant Product-Bound + vérification numérique.
Covers small cycles ($k \leq 1322$) by combining Product-Bound + numerical verification.
$k > 1322 \Rightarrow n < 2^{71}$
$k > 1322 \Rightarrow n < 2^{71}$
Hypothèse dérivée projet (combine BakerSeparation + gaps fractions continues log23 + Product Bound + BarinaVerification) — couvre les grands cycles. N'est pas un théorème publié : voir HYPOTHESES.md §5. Hercher 2023 (J. Integer Seq. 26.3.5) sur les m-cycles porte sur une quantité distincte (m = minima locaux, ≠ k = pas impairs).
A project-derived hypothesis (combines BakerSeparation + continued-fraction gaps of log23 + Product Bound + BarinaVerification) — covers large cycles. Not a published theorem: see HYPOTHESES.md §5. Hercher 2023 (J. Integer Seq. 26.3.5) on m-cycles addresses a distinct quantity (m = local minima, ≠ k = odd steps).
$(2^s - 3^k) \cdot k^6 \geq 3^k$
$(2^s - 3^k) \cdot k^6 \geq 3^k$
Forme effective sur $|S \log 2 - k \log 3|$ — axiome pivot (conjecture de travail, renforcement non démontré des bornes Rhin/Wu/Salikhov publiées — voir #28 et δ10) qui exclut les grands cycles ($k > 1322$) via continued fractions, sous condition que la conjecture tienne.
Effective form on $|S \log 2 - k \log 3|$ — pivotal axiom (working hypothesis (conjecture), undemonstrated strengthening of published Rhin/Wu/Salikhov bounds — see #28 and δ10) that excludes large cycles ($k > 1322$) via continued fractions, under the assumption that the conjecture holds.