spiral_return_exists and non_return in this chapter's data (labelled AXLE/Main_v6.lean) match no Lean file I could find: Main_v6.lean has no such theorem, and G.non_periodic_64 is not defined in any file I searched. In the author's latest file (AXLE_v6.lean, v6.2) the spiral-return theorem gtct_t1 assumes its conclusion as a hypothesis. A contraction orbit converges, so "generative, not periodic" is a heuristic, not a proved result. See book4/ch06.html.spiral_return_exists and non_return in this chapter's data (labelled AXLE/Main_v6.lean) match no Lean file I could find: Main_v6.lean has no such theorem, and G.non_periodic_64 is not defined in any file I searched. In the author's latest file (AXLE_v6.lean, v6.2) the spiral-return theorem gtct_t1 assumes its conclusion as a hypothesis. A contraction orbit converges, so "generative, not periodic" is a heuristic, not a proved result. See book4/ch06.html.Contração pitagórica $\kappa\leq\sqrt{5/9}<1$, ponto fixo único $x^*$, e $G^{64}(x_0)\neq x_0$
Pythagorean contraction $\kappa\leq\sqrt{5/9}<1$, unique fixed point $x^*$, and $G^{64}(x_0)\neq x_0$