Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

OEIS A400644: exact rounded recurrence

Abstract

The exact rounded three-term norm sequence has the Tribonacci square-root ratio limit.

Definition 1.1 (Source integer rounding operation).

Lean statement: D5/S1/Recurrence/OEISA400644.sourceRound

Formalization. D5/S1/Recurrence/OEISA400644.sourceRound (✓ std3).

Source. Repository-derived.

Commentary.

For every nonnegative integer radicand s, Nat.sqrt s is the lower integer candidate and the threshold s > r²+r selects r+1. This is the exact integer operation in the published Python source.

Theorem 1.2 (Two integer candidates bracket every source radicand).

Lean statement: D5/S1/Recurrence/OEISA400644.sourceRound_spec

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

Source. Repository-derived.

Commentary.

The integer square root brackets s between r² and (r+1)², and sourceRound s is exactly r or r+1.

Theorem 1.3 (Strict half-unit source rounding error).

Lean statement: D5/S1/Recurrence/OEISA400644.sourceRound_real_error

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

Source. Repository-derived.

Commentary.

Integer radicands cannot have a half-integer square root. Consequently the source operation differs from the real square root by strictly less than one half for every nonnegative integer radicand.

Definition 1.4 (The zero-based source sequence).

Lean statement: D5/S1/Recurrence/OEISA400644.a

Formalization. D5/S1/Recurrence/OEISA400644.a (✓ std3).

Source. Repository-derived.

Commentary.

The sequence starts 0, 0, 1 and applies the published rounded square-root recurrence at every later index. Source index n≥1 is represented by a(n−1).

Theorem 1.5 (Exact recurrence at every index).

Lean statement: D5/S1/Recurrence/OEISA400644.a_recurrence

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

Source. Repository-derived.

Commentary.

For every natural n, a(n+3) is exactly sourceRound of the sum of the three preceding squares.

Theorem 1.6 (The source sequence is monotone).

Lean statement: D5/S1/Recurrence/OEISA400644.a_mono

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

Source. Repository-derived.

Commentary.

Each term is at least the preceding term. This follows from the lower square-root candidate in the exact source rounding operation.

Theorem 1.7 (Eventual denominator positivity).

Lean statement: D5/S1/Recurrence/OEISA400644.a_pos

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

Source. Repository-derived.

Commentary.

Every term from the third zero-based term onward is at least one, so the eventual consecutive ratios have positive denominators.

Theorem 1.8 (Uniqueness of the recursively constructed sequence).

Lean statement: D5/S1/Recurrence/OEISA400644.a_unique

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

Source. Repository-derived.

Commentary.

Any natural-valued sequence with the same three initial values and the same exact recurrence agrees pointwise with a.

Theorem 1.9 (The Tribonacci square-root is the largest positive sextic root).

Lean statement: D5/S1/Recurrence/OEISA400644.rho_is_largest_positive_root

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

Source. Repository-derived.

Commentary.

rho is the positive square root of the Tribonacci constant. It satisfies rho⁶−rho⁴−rho²−1=0, and every positive real root of this polynomial is at most rho.

Definition 1.10 (Full infinite ratio limit target).

Lean statement: D5/S1/Recurrence/OEISA400644.targetClaim

Formalization. D5/S1/Recurrence/OEISA400644.targetClaim (✓ std3).

Source. Repository-derived.

Commentary.

The claim includes the infinite limit of a(n+3)/a(n+2), root identification, the exact positive-index recurrence, uniqueness on positive indices, positive denominators, and the same ratio limit for every sequence satisfying the published initial data and recurrence.

Theorem 1.11 (The exact infinite consecutive-ratio limit).

Lean statement: D5/S1/Recurrence/OEISA400644.result

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

Resolves. Problems/oeis-a400644-rounded-three-term-norm (proved) by D5/S1/Recurrence/OEISA400644.result.

Source. Repository-derived.

Commentary.

For the unique nonnegative integer sequence on positive indices with a(1)=a(2)=0 and a(3)=1, the recurrence a(n+1)=Round(sqrt(a(n)^2+a(n-1)^2+a(n-2)^2)) holds for every n at least 3. Its consecutive ratio tends to rho, the largest positive real root of x^6-x^4-x^2-1=0. Every denominator from the third positive index is positive.

The integer rounding threshold has strict error less than one half, so no tie convention changes any step. Monotonicity and the three-input square-root estimate give a(n+5) at least a(n+2)+1 in zero-based coordinates. Induction on blocks implies that the actual rounded terms tend to infinity.

Write lambda for the Tribonacci constant and b(n)=a(n+2)^2. The signed error e(n)=b(n+3)-b(n+2)-b(n+1)-b(n) satisfies |e(n)| at most 2 a(n+4). The positive projection T(n)=b(n+2)+(lambda-1)b(n+1)+b(n)/lambda obeys T(n+1)=lambda T(n)+e(n), with T(n) at least b(n+2). Hence e(n)/T(n) tends to zero and T(n+1)/T(n) tends to lambda.

The bounded coordinates v(n)=b(n+2)/T(n) lie in [0,1]. Their recurrence has limiting coefficients alpha=(lambda-1)/lambda and beta=lambda^(-3), both nonnegative with alpha+beta less than one. Put U=1/(1+alpha+beta). The deviations d(n)=v(n)-U satisfy d(n+2)=w(n)-alpha d(n+1)-beta d(n), where w(n) tends to zero because the coefficients converge and v is bounded.

For M(k)=max(|d(2k)|,|d(2k+1)|), the two-step estimate gives M(k+1) at most (alpha+beta)M(k)+(1+alpha)(|w(2k)|+|w(2k+1)|). The strict affine-contraction theorem yields M(k) tending to zero. Both parities are contained in these maxima, so v(n) tends to U over all natural indices. Since U is positive, b(n+3)/b(n+2) tends to lambda. Continuity of the real square root yields the original consecutive-ratio limit.

Finally rho^2=lambda converts the Tribonacci cubic into the sextic equation. Every positive sextic root x has x^2 greater than one and satisfies the Tribonacci cubic; cubic-root uniqueness forces x=rho. The shift sourceA(n)=a(n-1) gives the exact published indexing, and strong induction gives uniqueness on positive indices.

The theorem-specific typed registrations retain their compiled evidence. Source selections remain unresolved, with null certificates and source.selection_missing, under https://github.com/the-omega-institute/trureturing/issues/16003. No declared_validated status is asserted. The published statement and bounded literature scope are given in the A400644 problem dossier and its Library note.

References