bibkey: oeis2026a400644
authors: Bence Bernáth
year: 2026
title: "OEIS A400644, rounded three-term norm ratio"
doi: null
url: https://oeis.org/A400644
claim: "The consecutive ratio of the rounded three-term Euclidean-norm recurrence tends to the largest positive root of x^6-x^4-x^2-1 (conjecture)."
strata_touched:
  - D5/S1/Recurrence/OEISA400644
license: citation-only
triage: anchor

OEIS A400644 rounded three-term norm ratio

Problem

The published entry defines a(1)=a(2)=0, a(3)=1 and, for every n≥3, a(n+1)=Round(sqrt(a(n)^2+a(n-1)^2+a(n-2)^2)). It conjectures that the infinite consecutive ratio tends to 1.356203065626295..., the largest positive root of x^6-x^4-x^2-1.

The Lean source uses the exact zero-based correspondence a(0)=a(1)=0, a(2)=1; source index n is a(n-1) for n≥1.

Scope and status

Revision 28 and the displayed revision history through revision 1 are the bounded source scope. The verified source reading at 2026-10-12T21:39:40Z returned HTTP 200 and retained the conjectural wording in revision 28. No complete prior settlement was identified in that scope. The history’s informal convergence sentence does not supply an actual-sequence stability proof. The proved normalized-coordinate argument requires no infinite-product amplitude estimate. This note does not claim worldwide absence of another settlement.

Formal source

The D5 source defines the exact integer threshold and the zero-based sequence, proves source-rounding agreement, uniqueness and positivity, and contains the full infinite-limit result D5.S1.Recurrence.OEISA400644.result : targetClaim. Its proof uses the actual signed rounding error, a positive Tribonacci projection and a strict contraction of bounded normalized coordinates. The exact statement includes the positive-index correspondence and the unique sequence defined by the published recurrence. The formal result remains separate from an admitted external-resolution claim.

Verified locator

https://oeis.org/A400644

Evidence boundary

The source assessment covers revision 28, the complete displayed history through revision 1, rounding documentation, the four bounded arXiv abstract queries named in the Problems dossier, and repository and pinned Mathlib searches including private declarations. The history’s informal argument omits an actual-sequence stability proof. No complete settlement was found in this scope; offsite, inaccessible and unpublished proofs remain unverified.

The theorem-specific typed registrations remain declared_unresolved, with null certificates and source.selection_missing, under https://github.com/the-omega-institute/trureturing/issues/16003. All 16 compiled attempts are retained; no source-binding validation is asserted. The declaration inventory, proof shapes, consumers and retention boundaries are stated in Problems/oeis-a400644-rounded-three-term-norm.md.