slug: oeis-a400644-rounded-three-term-norm bibkey: oeis2026a400644 doi: null url: https://oeis.org/A400644 triage: theorem motivation_gids:

• D5/S0/Tower/Tribonacci/Values
• D5/S1/Recurrence/ComplementaryGoldenRatioLimit

OEIS A400644 rounded three-term norm ratio

Problem

OEIS A400644 revision 28 has the name:

a(n+1) = round(sqrt(a(n)^2 + a(n-1)^2 + a(n-2)^2)).

Its conjectural comment is:

Numerical evidence suggests that the ratio of consecutive terms (a(n+1)/a(n)) tends to 1.356203065626295… which is the largest positive real root of x^6-x^4-x^2-1=0. Setting x^2=t gives t^3-t^2-t-1 which yields the tribonacci constant (A058265) as the largest positive root.

The Mathematica source initializes a(1)=a(2)=0, a(3)=1 and uses Round[Sqrt[a[n]^2+a[n-1]^2+a[n-2]^2]]. The Python source starts [0,0,1], computes s as the sum of the last three squares, puts r=isqrt(s), and appends r+(s>r*r+r).

The target quantifies over the unique sequence with values in the nonnegative integers on every positive index and over every recurrence index n>=3. It asks for the full infinite consecutive-ratio limit.

Motivation

The published numerical conjecture is an external tier-1 question, preregistered at https://github.com/the-omega-institute/trureturing/issues/15948. The intended binding is ProblemSlug oeis-a400644-rounded-three-term-norm, GID D5/S1/Recurrence/OEISA400644.result, and ResolutionKind.Proved. The fixed initial data do not make this infinite asymptotic theorem a certified finite instance. Computational utility is none.

Gap

The bounded source assessment read revision 28 and every displayed revision 28 through 1 with the associated discussions. The earlier informal argument omits the implication from small local relative rounding error to stability of the actual consecutive ratios. Its divergent product indexed over all integer radicands is not a product along the actual sequence. This identifies a missing bridge in that argument; it does not refute the conjecture or exclude an unpublished completion.

The arXiv abstract searches were all:"A400644" (0 results), all:"rounded" AND all:"tribonacci" (0), all:"rounded" AND all:"Euclidean norm" (8), and all:"rounded" AND all:"recurrence" AND all:"limit" (22), with at most 30 results per query. None of the inspected returned abstracts supplied this exact theorem. These bounded searches do not establish global absence. Offsite complete proofs and inaccessible or unpublished sources remain unverified. The independently verified OEIS JSON, internal entry and history readings returned HTTP 200 and retained revision 28 with its conjectural wording (source reading: 2026-10-12T21:39:40Z). Revision 28 is the exact statement source. A complete prior published settlement would require reuse rather than a new resolved-problem claim.

Repository and pinned Mathlib searches include private declarations. The reusable Tribonacci root and strict affine-contraction results supply parts of the proof, but the linear unrounded Tribonacci ratio result does not prove the rounded recurrence’s limit.

Route

Use the exact zero-based sequence a(0)=a(1)=0, a(2)=1, and set sourceA(n)=a(n-1) on positive indices. Strict half-unit error proves agreement with nearest-integer rounding at every integer radicand; hence half-tie conventions cannot affect the recurrence. Strong induction proves uniqueness for every natural-valued sequence satisfying the source data.

Monotonicity and the square-root estimate give a(n+5)>=a(n+2)+1. A block induction implies divergence of the rounded terms. Put b(n)=a(n+2)^2 and e(n)=b(n+3)-b(n+2)-b(n+1)-b(n). Then |e(n)|<=2a(n+4) for the actual signed rounding error.

For the existing Tribonacci root lambda, define T(n)=b(n+2)+(lambda-1)b(n+1)+b(n)/lambda. Its coefficients are positive and T(n)>=b(n+2)>0. The cubic identity gives T(n+1)=lambda*T(n)+e(n). Thus e(n)/T(n)->0 and T(n+1)/T(n)->lambda.

The bounded coordinates v(n)=b(n+2)/T(n) lie in [0,1]. Their two-step recurrence has coefficient limits alpha=(lambda-1)/lambda, beta=lambda^(-3), with 0<=alpha, 0<=beta, alpha+beta<1. Let U=1/(1+alpha+beta)>0. The deviations from U obey a second-order stable recurrence with a vanishing error. The maxima of each pair of consecutive deviations satisfy the existing strict affine-contraction criterion. This covers both parities and proves v(n)->U for all indices. Quotient continuity now gives the squared ratio limit lambda, and square-root continuity gives the original ratio limit rho=sqrt(lambda). Positive-root uniqueness for the Tribonacci cubic identifies rho as the largest positive root of the exact sextic.

Falsifier

A mismatch in initial values, rounding or positive-index recurrence would invalidate source correspondence. A ratio limit for a finite prefix, a single parity or an unrounded trajectory does not prove this target. A failure to control the normalized coordinates over all indices would leave the analytic bridge unresolved.

Evidence

The mathematical source is D5/S1/Recurrence/OEISA400644.lean and its canonical exposition is Blueprint/D5/S1/Recurrence/OEISA400644.scribe.cs. The full result is D5.S1.Recurrence.OEISA400644.result : targetClaim. The theorem proves the full infinite source claim with no additional assumptions. The Reg mirror contains theorem-specific equivalence bridges, whole-family variation, sensitivity and observational-dependence proofs for all public targets. Its raw source-occurrence selections remain incomplete; no declared_validated registration is asserted. The exact typed attempts remain declared_unresolved, with null certificates and source.selection_missing, under the source-owner exception at https://github.com/the-omega-institute/trureturing/issues/16003. The issue records the 16 public targets and their missing source selections; it does not certify those selections. No active resolution claim is attached to an unfrozen result.

The per-declaration proof shapes below use the immutable frozen and pinned upstream boundary after inlining local helpers. They are semantic judgments, not machine-assigned statuses. Every auxiliary has an actual consumer on the proof path to result; its retention basis is that consumption. Only result has the tier-1 open-problem-resolution admission basis. No helper uses a standalone external-resolution exception. All declarations have semantic utility none: these are unbounded analytic statements or their definitions and proof steps, with no retained computational certificate, checker, enumeration or numerical-reduction declaration.

The definitions have no theorem proof-shape classification. Each is necessary in the exact statement or in the consumed proof, without a standalone admission basis.

Triage

Proved by D5/S1/Recurrence/OEISA400644.result: the decisive mechanism is the positive scalar projection together with a strict contraction of bounded relative coordinates. It avoids assuming that vanishing local error alone implies a ratio limit. The proof does not require an infinite-product amplitude estimate.

Extensions to other initial values or rounded higher-order norm recurrences remain open here. No adjacent result is included. The source comment’s numerical limit and root identification are the only external conclusion addressed; no additional source consequence is claimed.

ASSUMED-UNVERIFIED

No additional mathematical hypothesis is assumed in the closed result. Global novelty and absence of an offsite, inaccessible or unpublished complete proof are not established by the bounded source and literature searches. The current source-binding certificates for all 16 public audit targets remain unresolved under https://github.com/the-omega-institute/trureturing/issues/16003; the compiled typed attempts are retained, and none is described as declared_validated. Final independent reviews, required CI, merge and verification on dev remain necessary before resolved-problem credit.