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 associées à chacune des trois hypothèses H1-H3 (BakerSeparation, BarinaVerification, DerivedLargeKBound ; H3 est supposée, voir l'erratum).
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 associated with each of the three hypotheses H1-H3 (BakerSeparation, BarinaVerification, DerivedLargeKBound; H3 is assumed, see the erratum).
Pourquoi $\Lambda_{S,k}$ est le verrou central
Why $\Lambda_{S,k}$ is the central lock
Pour qu'un cycle Collatz hypothétique à $k$ termes impairs 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 hypothèse H1 BakerSeparation (paramètre des théorèmes, pas un axiome Lean) utilise la forme $(2^s - 3^k) \cdot k^6 \geq 3^k$ comme hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme : ce n'est pas un théorème publié — voir mea culpa #28.
For a hypothetical Collatz cycle with $k$ odd terms 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 hypothesis H1 BakerSeparation (a parameter of the theorems, not a Lean axiom) uses the form $(2^s - 3^k) \cdot k^6 \geq 3^k$ as a working hypothesis, stronger in this form than published effective bounds: it is not a published theorem — see mea culpa #28.
$n < 2^{71}$ vérifié
$n < 2^{71}$ verified
H2 : traduction d'un résultat de calcul publié (Bařina 2025, $n < 2^{71}$). Avec H1 (Product-Bound $n \leq (k^7+k)/3$), exclut les petits cycles ($k \leq 1322$).
H2: encoding of a published computational result (Barina 2025, $n < 2^{71}$). Together with H1 (Product-Bound $n \leq (k^7+k)/3$), excludes small cycles ($k \leq 1322$).
$k > 1322 \Rightarrow n < 2^{71}$
$k > 1322 \Rightarrow n < 2^{71}$
Hypothèse supposée, non dérivée ; sous H2, elle équivaut à la conclusion elle-même (en Lean, k est un temps de retour quelconque) (erratum du 2 octobre 2026). Les grands cycles ne sont donc exclus que par cette hypothèse. Voir HYPOTHESES.md, section H3 (ce fichier la présente comme une dérivation : c'est corrigé par l'erratum du 02/10/2026). Pour situer : Hercher (2023, J. Integer Seq. 26, Article 23.3.5) montre que, si la conjecture est vérifiée jusqu'à 3·2⁶⁹ (ce que couvre la vérification de Bařina, 2⁷¹), tout cycle non trivial a au moins 1,375·10¹¹ termes impairs. Ce n'est pas la source de H3.
An assumed hypothesis, not derived; under H2 it is equivalent to the conclusion itself (in Lean, k is any return time) (erratum of 2 October 2026). Large cycles are therefore excluded only by this hypothesis. See HYPOTHESES.md, section H3 (that file presents it as a derivation: corrected by the erratum of 2 Oct 2026). For context: Hercher (2023, J. Integer Seq. 26, Article 23.3.5) shows that, if the conjecture is verified up to 3·2⁶⁹ (covered by Barina's verification, 2⁷¹), every non-trivial cycle has at least 1.375·10¹¹ odd terms. This is not the source of H3.
$(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|$ — hypothèse H1 (paramètre ; hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme — voir mea culpa #28). Dans le code publié, elle sert au Product-Bound $n \leq (k^7+k)/3$, donc au cas $k \leq 1322$. Les grands cycles ($k > 1322$) sont exclus uniquement par l'hypothèse supposée H3 (avec H2).
Effective form on $|S \log 2 - k \log 3|$ — hypothesis H1 (parameter; working hypothesis, stronger in this form than published effective bounds — see mea culpa #28). In the published code it serves the Product-Bound $n \leq (k^7+k)/3$, hence the case $k \leq 1322$. Large cycles ($k > 1322$) are excluded only by the assumed hypothesis H3 (with H2).