LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The coded curves are genuine $C^{1}$ stable and unstable curves of $F$ , with transverse intersection at every finite-word homoclinic point

Statement

Fix $a \geq 100$ and let $R = \sqrt{a} + 3$ , $L = \sqrt{a - 2 R}$ , $F (x, y) = (y, y^{2} - a - x)$ , $x (s)$ , $h$ and the sets $W^{s}, W^{u}$ be as in The two-sign bilateral shift space, its coding map, and the ball of bounded bilateral real sequences, The square-root recurrence $T_{s} (x)_{n} = s_{n} \sqrt{a + x_{n - 1} + x_{n + 1}}$ is a contraction of $B_{R}$ with a unique coded solution, Finite symbol windows determine the code: locality of the iterates, coding continuity and injectivity of $h (σ) = (x_{- 1} (σ), x_{0} (σ))$ and Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family. For $u \in {- 1, + 1}$ put $r_{u} : = 1 + u \sqrt{a + 1}$ and let

$M_{u}^{\sqrt{}} (v, w) : = u \sqrt{a + v + w}$

be the square-root update of the coded recurrence. Then:

(hyperbolicity) the fixed points $(r_{u}, r_{u})$ of $F$ are hyperbolic: $D F (r_{u}, r_{u})$ has two real eigenvalues, one of modulus $> 1$ and one of modulus $< 1$ ;
(stable curve at a finite-word point) let $s \in X_{\pm}$ be nonconstant with $s_{n} = u$ for $∣ n ∣ \geq N$ , and put $z_{*} : = h (s)$ . Then there are $δ_{s} > 0$ and a $C^{1}$ curve $γ_{s} : (- δ_{s}, δ_{s}) \to R^{2}$ with $γ_{s} (0) = z_{*}$ , $γ_{s} ((- δ_{s}, δ_{s})) \subseteq W^{s} (r_{u}, r_{u})$ and tangent $γ_{s}^{'} (0) \in C_{1 / 2}^{s}$ ;
(unstable curve at a finite-word point) likewise there are $δ_{u} > 0$ and a $C^{1}$ curve $γ_{u} : (- δ_{u}, δ_{u}) \to R^{2}$ with $γ_{u} (0) = z_{*}$ , $γ_{u} ((- δ_{u}, δ_{u})) \subseteq W^{u} (r_{u}, r_{u})$ and $γ_{u}^{'} (0) \in C_{1 / 2}^{u}$ ; consequently $z_{*}$ is a transverse homoclinic point of $(r_{u}, r_{u})$ (Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family);
(local stable and unstable sets at the fixed point) put $ρ : = 1 / 8$ and define $∥ (x, y) ∥_{\max} : = \max (∣ x ∣, ∣ y ∣)$ . Then the set of points $y = (y_{- 1}, y_{0}) \in R^{2}$ whose forward orbit stays within max-norm distance $ρ$ of $(r_{u}, r_{u})$ ,

$Γ_{ρ}^{s} : = {y : ∥ F^{n} (y) - (r_{u}, r_{u}) ∥_{\max} \leq ρ for every n \geq 0},$

is exactly the graph ${(b, r_{u} + u_{0} (b)) : ∣ b - r_{u} ∣ \leq ρ}$ of the half-tail solution map $b \mapsto u_{0} (b)$ obtained from [F2] with the constant reference $y_{n} : = r_{u}$ and $b_{*} : = r_{u}$ ; in particular it is a $C^{1}$ embedded curve through $(r_{u}, r_{u})$ whose tangent at the fixed point lies in $C_{1 / 2}^{s}$ . With $Σ (x, y) : = (y, x)$ the same statement holds in the unstable direction: a point has all its backward iterates $F^{- n} (y)$ within max-norm distance $ρ$ of $(r_{u}, r_{u})$ if and only if it lies in $Σ (Γ_{ρ}^{s})$ , and $Σ (Γ_{ρ}^{s})$ is a $C^{1}$ embedded curve through $(r_{u}, r_{u})$ whose tangent lies in $C_{1 / 2}^{u}$ .

Facts & Assumptions

Given: The parameter $a \geq 100$ , the constants $R, L$ , the coded sequences $x (s)$ , the coding map $h$ , the fixed points $r_{u}$ , the square-root updates $M_{u}^{\sqrt{}}$ , and a nonconstant code $s$ with $s_{n} = u$ for $∣ n ∣ \geq N$ .

[F1]

Coding data (The square-root recurrence $T_{s} (x)_{n} = s_{n} \sqrt{a + x_{n - 1} + x_{n + 1}}$ is a contraction of $B_{R}$ with a unique coded solution, Finite symbol windows determine the code: locality of the iterates, coding continuity and injectivity of $h (σ) = (x_{- 1} (σ), x_{0} (σ))$ , The quadratic map $F (x, y) = (y, y^{2} - a - x)$ has a compact coded invariant set conjugate to the two-sign shift, with chaos under ${A C}_{ω}$ ): $x_{n} (s) = M_{s_{n}}^{\sqrt{}} (x_{n - 1} (s), x_{n + 1} (s))$ , $∣ x_{n} (s) ∣ \in [L, R]$ , and $F (h (s)) = h (S_{\pm} s)$ ; moreover $∣ x_{n} (s) ∣ \leq \sqrt{a + 2 R} < R$ and $R - \sqrt{a + 2 R} = (4 \sqrt{a} + 3) / (R + \sqrt{a + 2 R}) > (4 \sqrt{a} + 3) / (2 R) > 1 / 2$ , since $R^{2} - (a + 2 R) = 4 \sqrt{a} + 3$ .

[F2]

Weighted half-tail lemma (Weighted half-tail contractions for $q_{n} = M_{s_{n}} (q_{n - 1}, q_{n + 1})$ give a unique $C^{1}$ curve with tangent slope bounded by $c / (1 - q)$ ): for θ=1/2, q=c(θ+θ⁻¹)<1, a compact interval J, a reference half-orbit, and a local parameter interval I satisfying the lemma's radius and margin hypotheses, T_b is a contraction of the closed weighted ball of radius ρ̄ into itself for b∈I. Its unique fixed points u(b) are C¹ in b, satisfy ‖u(b)‖θ≤c|b−b*|/(1−q), and the phase curve b↦(b,y₀+u₀(b)) has tangent (1,d₀) with |d₀|≤c/(1−q); its forward orbit tracks the reference with deviations bounded by ‖u(b)‖_θ.

[F3]

Homoclinic and constant-code data (Constant codes give the fixed points, and finite nonconstant word codes give homoclinic orbits converging to a fixed point at both ends): the constant code $\overset{ˉ}{u}$ has $x_{n} (\overset{ˉ}{u}) = r_{u}$ with $r_{u}^{2} = a + 2 r_{u}$ and $sign (r_{u}) = u$ ; for a finite-word code $s$ , $F^{n} (h (s)) \to (r_{u}, r_{u})$ as $n \to \pm \infty$ , and $h (s) \neq (r_{u}, r_{u})$ when $s \neq \overset{ˉ}{u}$ .

[F4]

The reflection symmetry (Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder): with $Σ (x, y) : = (y, x)$ one has $Σ^{2} = i d$ , $Σ \circ F \circ Σ = F^{- 1}$ (because $Σ F Σ (x, y) = Σ F (y, x) = Σ (x, x^{2} - a - y) = (x^{2} - a - y, x) = F^{- 1} (x, y)$ ), and $Σ$ maps $C_{1 / 2}^{s}$ onto $C_{1 / 2}^{u}$ .

[F5]

Hyperbolic fixed points (Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Absolute value in an ordered field, Basic properties of the absolute value, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ): $D F (x, y) = (\begin{array}{cc} 0 & 1 \\ - 1 & 2 y \end{array})$ ; the characteristic polynomial at $(r_{u}, r_{u})$ is $λ^{2} - 2 r_{u} λ + 1$ , with roots $r_{u} \pm \sqrt{r_{u}^{2} - 1}$ . Here $r_{+} = 1 + \sqrt{a + 1} > 1$ and $r_{-} = 1 - \sqrt{a + 1} < - 1$ , so the supplier's definition tests whether each eigenvalue has modulus different from $1$ .

[F6]

Convergence and continuity (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, $C^{k}$ Euclidean maps and diffeomorphisms): the definitions of convergence in $R^{2}$ , of $C^{1}$ curves on an interval, and of the stable and unstable sets of Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family.

[F7]

One-sided bounded sequences and the deviation operator (The bounded functions on a set form a complete metric space in the supremum metric, and the coding map of the two-sign shift space is an isometry, clause 4, Constant codes give the fixed points, and finite nonconstant word codes give homoclinic orbits converging to a fixed point at both ends, Absolute value in an ordered field, Basic properties of the absolute value, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ): let $ρ = 1 / 8$ . For either sign, $∣ r_{u} ∣ = \sqrt{a + 1} - 1$ or $1 + \sqrt{a + 1}$ , so $∣ r_{u} ∣ > 9$ for $a \geq 100$ . If $∣ b - r_{u} ∣ \leq ρ$ and $v, w : N \to R$ have $∥ v ∥_{\infty}, ∥ w ∥_{\infty} \leq ρ$ , then in the update $(T_{b} v)_{n} : = M_{u}^{\sqrt{}} (r_{u} + v_{n - 1}, r_{u} + v_{n + 1}) - r_{u}, v_{- 1} : = b - r_{u},$ every radicand lies in $[r_{u}^{2} - 1 / 4, r_{u}^{2} + 1 / 4] \subset (64, \infty)$ , so $T_{b}$ is defined. For each $n \geq 1$ the difference of two outputs is at most $(∣ v_{n - 1} - w_{n - 1} ∣ + ∣ v_{n + 1} - w_{n + 1} ∣) / 16$ ; at $n = 0$ it is at most $∣ v_{1} - w_{1} ∣ / 16$ . Thus $∥ T_{b} v - T_{b} w ∥_{\infty} \leq (1 / 8) ∥ v - w ∥_{\infty}$ .

Proof

technique · direct; solve the two slope-free half-tail problems for the square-root update, use the reflection symmetry for the unstable direction, and read off hyperbolicity and transversality

1.1givenF5algebra

Hyperbolicity: the characteristic polynomial in [F5] has the two real roots $r_{u} \pm \sqrt{r_{u}^{2} - 1}$ , whose product is $1$ . If $u = + 1$ , then $r_{u} > 1$ , so $r_{u} + \sqrt{r_{u}^{2} - 1} > 1$ and $r_{u} - \sqrt{r_{u}^{2} - 1} = 1 / (r_{u} + \sqrt{r_{u}^{2} - 1}) \in (0, 1)$ . If $u = - 1$ , write $r_{u} = - m$ with $m > 1$ ; then $r_{u} - \sqrt{r_{u}^{2} - 1} < - 1$ and $r_{u} + \sqrt{r_{u}^{2} - 1} = - 1 / (m + \sqrt{m^{2} - 1}) \in (- 1, 0)$ . Thus each fixed point has one eigenvalue of modulus greater than $1$ and one of modulus less than $1$ , proving clause 1 by the hyperbolicity definition of Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family.

2.1givenstep 1.1F1F2F3algebra

Stable curve: apply [F2] with $θ : = 1 / 2$ , $J : = [- R, R]$ , $c : = 1 / 16$ , $q : = 5 / 32$ , the update $M_{s_{n}}^{\sqrt{}}$ , reference $y_{n} : = x_{n} (s)$ $(n \geq 0)$ , $b_{*} : = x_{- 1} (s)$ , $\overset{ˉ}{ρ} : = 1 / 2$ , and $δ_{*} : = 1 / 4$ . By [F1], $∣ y_{n} ∣ \geq L > 1 / 2$ and $∣ y_{n} ∣ \leq \sqrt{a + 2 R} < R - 1 / 2$ , so the margin condition holds; also $∣ b_{*} ∣ < R - 1 / 2$ , so $[b_{*} - δ_{*}, b_{*} + δ_{*}] \subseteq J$ , and $δ_{*} < (1 - q) \overset{ˉ}{ρ} / c$ . The updates are $C^{2}$ on the open set $a + v + w > 0$ , containing $J \times J$ , with first partials $u / (2 \sqrt{a + v + w})$ and second partials $- u / (4 (a + v + w)^{3 / 2})$ . On $J \times J$ their first partials have absolute value at most $1 / (2 L) < 1 / 16$ , since $L \geq \sqrt{74} > 8$ , and $∣ M_{u}^{\sqrt{}} ∣ \leq \sqrt{a + 2 R} < R$ . Thus their extensions, image and derivative bounds match every premise of [F2]. The recurrence holds by [F1]. Hence there is a $C^{1}$ curve $b \mapsto Z (b) : = (b, x_{0} (b))$ through $Z (b_{*}) = (x_{- 1} (s), x_{0} (s)) = z_{*}$ with tangent $(1, d_{0})$ and $∣ d_{0} ∣ \leq c / (1 - q) = 2 / 27 < 1 / 2$ . Every point $Z (b)$ has forward orbit tracking the reference orbit $F^{n} (z_{*})$ , which converges to $(r_{u}, r_{u})$ by [F3]; hence $Z (b)$ lies in $W^{s} (r_{u}, r_{u})$ and its tangent lies in $C_{1 / 2}^{s}$ . This proves clause 2.

3.1givenstep 2.1F1F2F3F4algebra

Unstable curve: put $w : = Σ (z_{*}) = (x_{0} (s), x_{- 1} (s))$ and let $y_{n} : = x_{- n - 1} (s)$ for $n \geq 0$ , with boundary value $b_{*} : = x_{0} (s)$ . By the recurrence of [F1], this is a reference half-orbit for the square-root update, and $∣ y_{n} ∣ \geq L > 1 / 2$ , $∣ y_{n} ∣ \leq \sqrt{a + 2 R} < R - 1 / 2$ . Apply [F2] with $θ = 1 / 2$ , $J = [- R, R]$ , $c = 1 / 16$ , $q = 5 / 32$ , $\overset{ˉ}{ρ} = 1 / 2$ , and $δ_{*} = 1 / 4$ ; the margin and parameter-interval conditions hold by [F1]. The resulting $C^{1}$ curve through $w$ has tangent $(1, d_{0})$ with $∣ d_{0} ∣ \leq 2 / 27$ , and its forward orbits track that of $w$ : by [F4], $F^{n} (w) = Σ (F^{- n} (z_{*}))$ , which converges to $(r_{u}, r_{u})$ by [F3]. Reflecting the curve by $Σ$ gives a $C^{1}$ curve $γ_{u}$ through $z_{*}$ , tangent $(d_{0}, 1) \in C_{1 / 2}^{u}$ , whose points lie in $W^{u} (r_{u}, r_{u})$ . This proves clause 3.

3.2givenstep 1.1step 2.1F1F2F4

Local stable set: apply [F2] with $θ = 1 / 2$ , $J = [- R, R]$ , $c = 1 / 16$ , $q = 5 / 32$ , $\overset{ˉ}{ρ} = 1 / 8$ , $δ_{*} = 1 / 4$ , the constant symbols $s_{n} : = u$ , constant reference $y_{n} : = r_{u}$ , and $b_{*} : = r_{u}$ . The reference satisfies the recurrence because $r_{u}^{2} = a + 2 r_{u}$ and $sign (r_{u}) = u$ , so $r_{u} = M_{u}^{\sqrt{}} (r_{u}, r_{u})$ by [F3]. By [F7], $∣ r_{u} ∣ > 9$ , and $∣ r_{u} ∣ \leq \sqrt{a + 2 R} < R - 1 / 2$ , so the reference-margin condition and $[r_{u} - δ_{*}, r_{u} + δ_{*}] \subseteq J$ hold; also $δ_{*} < (1 - q) \overset{ˉ}{ρ} / c = 27 / 16$ . Hence there is a $C^{1}$ map $b \mapsto u (b)$ with $∥ u (b) ∥_{θ} \leq (c / (1 - q)) ∣ b - r_{u} ∣ = (2 / 27) ∣ b - r_{u} ∣$ . Define $Γ : = {(b, r_{u} + u_{0} (b)) : ∣ b - r_{u} ∣ \leq ρ}$ with $ρ : = 1 / 8$ ; this closed parameter interval lies inside $I$ because $δ_{*} = 1 / 4$ .

4.1step 2.1step 3.1F4

Transversality: by steps 2.1 and 3.1 the tangent of $γ_{s}$ at $z_{*}$ lies in $C_{1 / 2}^{s}$ and that of $γ_{u}$ in $C_{1 / 2}^{u}$ ; since $C_{1 / 2}^{s} \cap C_{1 / 2}^{u} = {0}$ ([F4], Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family) the two tangent lines are distinct, so the two curves cross transversely at $z_{*}$ . This is the transversality assertion of clause 3.

4.2step 3.2F1F2F4algebra

The graph lies in the trapping set: let $∣ b - r_{u} ∣ \leq ρ$ and put $x_{- 1} : = b$ , $x_{n} : = r_{u} + u_{n} (b)$ for $n \geq 0$ . By the fixed-point equation of [F2], the sequence satisfies $x_{n} = M_{u}^{\sqrt{}} (x_{n - 1}, x_{n + 1})$ for every $n \geq 0$ , so $F (x_{n - 1}, x_{n}) = (x_{n}, x_{n + 1})$ by [F1] and $F^{n} (b, x_{0}) = (x_{n - 1}, x_{n})$ for all $n \geq 0$ . Also $∣ x_{- 1} - r_{u} ∣ = ∣ b - r_{u} ∣ \leq ρ$ and $∣ x_{n} - r_{u} ∣ \leq ∥ u (b) ∥_{θ} \leq (2 / 27) ∣ b - r_{u} ∣ \leq ρ$ for $n \geq 0$ . Thus every point of $Γ$ has all forward iterates within max-norm distance $ρ$ of $(r_{u}, r_{u})$ .

4.3givenstep 3.2F1F2F6F7algebra

The trapping set lies in the graph: let $y = (y_{- 1}, y_{0})$ satisfy $∥ F^{n} (y) - (r_{u}, r_{u}) ∥_{\max} \leq ρ$ for every $n \geq 0$ , and write $F^{n} (y) = (ξ_{n - 1}, ξ_{n})$ . Then $∣ ξ_{n} - r_{u} ∣ \leq ρ$ for every $n \geq - 1$ . Since $∣ r_{u} ∣ > 9$ by [F7], each $ξ_{n}$ has sign $u$ and $∣ ξ_{n} ∣ > 8$ . The orbit identity $ξ_{n + 1} = ξ_{n}^{2} - a - ξ_{n - 1}$ gives $a + ξ_{n - 1} + ξ_{n + 1} = ξ_{n}^{2} > 64$ , so for $n \geq 0$ one has $ξ_{n} = u \sqrt{a + ξ_{n - 1} + ξ_{n + 1}} = M_{u}^{\sqrt{}} (ξ_{n - 1}, ξ_{n + 1})$ . Put $v_{n} : = ξ_{n} - r_{u}$ for $n \geq 0$ and $b : = y_{- 1}$ . Then $∥ v ∥_{\infty} \leq ρ$ , $∣ b - r_{u} ∣ \leq ρ$ , and the displayed identity says exactly $(T_{b} v)_{n} = v_{n}$ for all $n \geq 0$ . The weighted solution $u (b)$ from step 3.2 also satisfies $T_{b} u (b) = u (b)$ and $∥ u (b) ∥_{\infty} \leq ∥ u (b) ∥_{θ} \leq (2 / 27) ∣ b - r_{u} ∣ < ρ$ . By [F7], $∥ v - u (b) ∥_{\infty} = ∥ T_{b} v - T_{b} u (b) ∥_{\infty} \leq (1 / 8) ∥ v - u (b) ∥_{\infty}$ , so $v = u (b)$ and $y = (y_{- 1}, r_{u} + u_{0} (y_{- 1})) \in Γ$ .

5.1step 4.1step 4.2step 4.3F2F4

Local stable set identified: steps 4.2 and 4.3 show that the set $Γ_{ρ}^{s}$ of clause 4 equals $Γ$ ; by [F2] and step 4.1 the curve $Γ$ is $C^{1}$ with tangent $(1, d_{0})$ at the fixed point and $∣ d_{0} ∣ \leq c / (1 - q) \leq 2 / 27 < \frac{1}{2}$ , so the tangent lies in $C_{1 / 2}^{s}$ . This is the stable half of clause 4.

6.1step 4.3step 5.1F4F6∎

Local unstable set: by [F4], $F^{- 1} = Σ F Σ$ with $Σ^{2} = i d$ , and $Σ$ preserves the max norm because it permutes coordinates. Hence for every $y$ and $n \geq 0$ , $∥ F^{- n} (y) - (r_{u}, r_{u}) ∥_{\max} = ∥ F^{n} (Σ y) - (r_{u}, r_{u}) ∥_{\max}$ . Therefore the set of points whose backward orbit stays within max-norm distance $ρ$ of $(r_{u}, r_{u})$ is exactly $Σ (Γ_{ρ}^{s}) = Σ (Γ)$ . Its tangent at $(r_{u}, r_{u})$ is $Σ (1, d_{0}) = (d_{0}, 1) \in C_{1 / 2}^{u}$ because $Σ$ maps $C_{1 / 2}^{s}$ onto $C_{1 / 2}^{u}$ by [F4], and it is a $C^{1}$ embedded curve as the image under a linear homeomorphism. This completes the proof of clause 4.

Remarks

Clause 4 identifies the local stable and unstable sets of the fixed points with the constructed graphs, which is the piece of the stable-manifold picture used by the transversality argument; no global stable-manifold theorem and no structural-stability theorem is invoked.
The unstable curve is obtained from the stable construction by the exact reflection symmetry $Σ F Σ = F^{- 1}$ of the quadratic family; this avoids a separate backward half-tail contraction.
The aperture $1 / 2$ is the one used throughout; the derivative bound $∣ d_{0} ∣ \leq 1 / 2$ is verified with the explicit bound $L \geq \sqrt{74}$ and is not claimed to be optimal.

The coded curves are genuine $C^{1}$ stable and unstable curves of $F$ , with transverse intersection at every finite-word homoclinic point

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

The coded curves are genuine C1C1 stable and unstable curves of FF, with transverse intersection at every finite-word homoclinic point

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

The coded curves are genuine $C^{1}$ stable and unstable curves of $F$ , with transverse intersection at every finite-word homoclinic point