Bernáth’s OEIS A400645 consecutive-ratio limit

Abstract

The signed four-lag rounded norm sequence has Bernáth’s exact ratio limit.

Definition 1.1 (The signed four-square radicand).

$$\forall a:(\mathbb{N}\to \mathbb{N}),\forall n:(\mathbb{N}),\mathrm{radicand}\left(a,n\right)=((a\left(n\right):\mathbb{Z}){)}^2+((a\left(n-1\right):\mathbb{Z}){)}^2+((a\left(n-2\right):\mathbb{Z}){)}^2-((a\left(n-3\right):\mathbb{Z}){)}^2$$

Formalization. D5/S1/Recurrence/OEISA400645.radicand (✓ std3).

Citation. Bence Bernáth (2026). OEIS A400645, signed four-lag rounded norm ratio. URL: https://oeis.org/A400645.

Commentary.

a(n+1) = round(sqrt(a(n)^2 + a(n-1)^2 + a(n-2)^2 - a(n-3)^2)). Source: OEIS A400645, revision 21, NAME field (unpaginated). The four squares are integers; the predecessor indices use natural subtraction.

Definition 1.2 (The positive-index recurrence and initial values).

$$\forall a:(\mathbb{N}\to \mathbb{N}),\mathrm{IsSourceSequence}\left(a\right)=((a\left(1\right)=0)\wedge ((a\left(2\right)=0)\wedge ((a\left(3\right)=0)\wedge ((a\left(4\right)=1)\wedge (\forall n:(\mathbb{N}),(4\le n)\Rightarrow ((0\le \mathrm{radicand}\left(a,n\right))\wedge ((a\left(n+1\right):\mathbb{Z})=\mathrm{round}\left(\mathrm{Real}.\mathrm{sqrt}\left((\mathrm{radicand}\left(a,n\right):\mathbb{R})\right)\right))))))))$$

Formalization. D5/S1/Recurrence/OEISA400645.IsSourceSequence (✓ std3).

Citation. Bence Bernáth (2026). OEIS A400645, signed four-lag rounded norm ratio. URL: https://oeis.org/A400645.

Commentary.

a(n+1) = round(sqrt(a(n)^2 + a(n-1)^2 + a(n-2)^2 - a(n-3)^2)). The Mathematica field states a[1] == a[2] == a[3] == 0, a[4] == 1. Source: OEIS A400645, revision 21, NAME and Mathematica fields (unpaginated). The recurrence applies for n ≥ 4; index zero is unused. Nonnegativity of the signed radicand is explicit.

Definition 1.3 (The cross-referenced quartic constant).

$$(squaredLimit:\mathbb{R})=\frac{1+\mathrm{Real}.\mathrm{sqrt}\left(13\right)+\mathrm{Real}.\mathrm{sqrt}\left(2\cdot \mathrm{Real}.\mathrm{sqrt}\left(13\right)-2\right)}{4}$$

Formalization. D5/S1/Recurrence/OEISA400645.squaredLimit (✓ std3).

Citation. Bence Bernáth (2026). OEIS A400645, signed four-lag rounded norm ratio. URL: https://oeis.org/A400645.

Commentary.

Equals (1 + sqrt(13) + sqrt(2*sqrt(13) - 2))/4. - Vaclav Kotesovec, Aug 27 2021. Source: OEIS A289917, revision 48, FORMULA field (unpaginated), cross-referenced by A400645.

Definition 1.4 (The conjectured consecutive-ratio limit).

$$(limitingRatio:\mathbb{R})=\mathrm{Real}.\mathrm{sqrt}\left(squaredLimit\right)$$

Formalization. D5/S1/Recurrence/OEISA400645.limitingRatio (✓ std3).

Citation. Bence Bernáth (2026). OEIS A400645, signed four-lag rounded norm ratio. URL: https://oeis.org/A400645.

Commentary.

Numerical evidence suggests that the ratio of consecutive terms (a(n+1)/a(n)) tends to 1.3122819079… (sqrt(A289917)) which is the largest real root of the asymptotic equation of this sequence: x^8-x^6-x^4-x^2+1. Source: OEIS A400645, revision 21, COMMENTS field (unpaginated). The value sqrt(A289917) is Real.sqrt squaredLimit.

Definition 1.5 (The full infinite limit and largest-root assertion).

$$claim=((\exists a:(\mathbb{N}\to \mathbb{N}),\mathrm{IsSourceSequence}\left(a\right))\wedge ((\forall a:(\mathbb{N}\to \mathbb{N}),(\mathrm{IsSourceSequence}\left(a\right))\Rightarrow (\forall e:(\mathbb{R}),(0<e)\Rightarrow (\exists N:(\mathbb{N}),(4\le N)\wedge (\forall n:(\mathbb{N}),(N\le n)\Rightarrow ((0<a\left(n\right))\wedge (|\frac{(a\left(n+1\right):\mathbb{R})}{(a\left(n\right):\mathbb{R})}-limitingRatio|<e))))))\wedge (((limitingRatio{)}^8-(limitingRatio{)}^6-(limitingRatio{)}^4-(limitingRatio{)}^2+1=0)\wedge (\forall x:(\mathbb{R}),((x{)}^8-(x{)}^6-(x{)}^4-(x{)}^2+1=0)\Rightarrow (x\le limitingRatio)))))$$

Formalization. D5/S1/Recurrence/OEISA400645.claim (✓ std3).

Citation. Bence Bernáth (2026). OEIS A400645, signed four-lag rounded norm ratio. URL: https://oeis.org/A400645.

Commentary.

Numerical evidence suggests that the ratio of consecutive terms (a(n+1)/a(n)) tends to 1.3122819079… (sqrt(A289917)) which is the largest real root of the asymptotic equation of this sequence: x^8-x^6-x^4-x^2+1. This is related to A116732 where the asymptotic equation is y^4-y^3-y^2-y+1 via y=x^2. Source: OEIS A400645, revision 21, COMMENTS field (unpaginated). Natural indices start at 1. Subtraction in the radicand is in ℤ, and nearest rounding produces an integer. Existence, eventual positive denominators and the largest real root are included.

Theorem 1.6 (The signed rounded recurrence has the stated infinite limit).

$$(\exists a:(\mathbb{N}\to \mathbb{N}),\mathrm{IsSourceSequence}\left(a\right))\wedge ((\forall a:(\mathbb{N}\to \mathbb{N}),(\mathrm{IsSourceSequence}\left(a\right))\Rightarrow (\forall e:(\mathbb{R}),(0<e)\Rightarrow (\exists N:(\mathbb{N}),(4\le N)\wedge (\forall n:(\mathbb{N}),(N\le n)\Rightarrow ((0<a\left(n\right))\wedge (|\frac{(a\left(n+1\right):\mathbb{R})}{(a\left(n\right):\mathbb{R})}-limitingRatio|<e))))))\wedge (((limitingRatio{)}^8-(limitingRatio{)}^6-(limitingRatio{)}^4-(limitingRatio{)}^2+1=0)\wedge (\forall x:(\mathbb{R}),((x{)}^8-(x{)}^6-(x{)}^4-(x{)}^2+1=0)\Rightarrow (x\le limitingRatio))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/OEISA400645.result (✓ std3). ∎

Resolves. Problems/bernath-a400645 (proved) by D5/S1/Recurrence/OEISA400645.result.

Source. Repository-derived.

Acknowledgement. Bence Bernáth (2026). OEIS A400645, signed four-lag rounded norm ratio. URL: https://oeis.org/A400645.

Commentary.

The integer rounding bound and monotonicity give a Fibonacci upper estimate. With squaredLimit greater than 17/10, the rounding errors grow more slowly than the dominant mode. The exact value a(26)=324 controls the entire infinite error tail and gives a positive normalized projection limit above 73872/17. A weighted three-coordinate contraction gives a positive limit for normalized squares. Division and continuity of Real.sqrt give the consecutive-ratio limit. The quartic factorization identifies the largest octic root.

References

• Truth anchor: D5/S1/Recurrence/OEISA400645.IsSourceSequence
• Truth anchor: D5/S1/Recurrence/OEISA400645.claim
• Truth anchor: D5/S1/Recurrence/OEISA400645.limitingRatio
• Truth anchor: D5/S1/Recurrence/OEISA400645.radicand
• Truth anchor: D5/S1/Recurrence/OEISA400645.result
• Truth anchor: D5/S1/Recurrence/OEISA400645.squaredLimit
• Dependency: D5/S0/Tower/NonPisotFrontier/BetaThirteen
• Dependency: D5/S1/Recurrence/ComplementaryGoldenRatioLimit
• Dependency: D5/S1/Recurrence/OEISA400644