1. FormalConjectures
  2. OEIS
  3. «100434»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Expansion of g.f. $(1+x)(3+x)/(1+6x^2+x^4)$

This sequence is defined by the linear recurrence relation $a(n) = -6 a(n-2) - a(n-4)$ for $n \ge 4$, with initial values $a(0)=3$, $a(1)=4$, $a(2)=-17$, $a(3)=-24$.

References:

namespace OeisA100434

The primary defining sequence a, which is the expansion of the generating function $(1+x)(3+x)/(1+6x^2+x^4)$. It satisfies the recurrence $a(n) = -6 a(n-2) - a(n-4)$ for $n \ge 4$.

def a : ℕ → ℤ | 0 => 3 | 1 => 4 | 2 => -17 | 3 => -24 | n + 4 => -6 * a (n + 2) - a n

$c(n)$ starts with $(1, -3, -7, 17)$ and satisfies the same recurrence as a

def c : ℕ → ℤ | 0 => 1 | 1 => -3 | 2 => -7 | 3 => 17 | n + 4 => -6 * c (n + 2) - c n

$d(n)$ starts with $(2, 4, -10, -24)$ and satisfies the same recurrence as a

def d : ℕ → ℤ | 0 => 2 | 1 => 4 | 2 => -10 | 3 => -24 | n + 4 => -6 * d (n + 2) - d n

$b(2n) = -c(2n+1)$, $b(2n+1) = c(2n)$

-- Sign corrected (even branch): see https://github.com/google-deepmind/formal-conjectures/issues/5025 def b (n : ℕ) : ℤ := if n % 2 = 0 then -c (n + 1) else c (n - 1)

$e(2n) = d(2n)/2$, $e(2n+1) = - d(2n)/2$

def e (n : ℕ) : ℤ := if n % 2 = 0 then d n / 2 else -- n is positive, so n-1 is safe in ℕ - (d (n - 1) / 2)

$f(2n) = f(2n+1) = d(2n+1)/2$

def f (n : ℕ) : ℤ := let m := n / 2 d (2 * m + 1) / 2

$g(2n) = 0, g(2n+1) = c(2n+1)$

def g (n : ℕ) : ℤ := if n % 2 = 0 then 0 else c n

Value of the sequence a at 0.

@[category test, AMS 11] theorem a_0 : a 0 = 3 := ⊢ a 0 = 3 All goals completed! 🐙

Value of the sequence a at 1.

@[category test, AMS 11] theorem a_1 : a 1 = 4 := ⊢ a 1 = 4 All goals completed! 🐙

Value of the sequence a at 2.

@[category test, AMS 11] theorem a_2 : a 2 = -17 := ⊢ a 2 = -17 All goals completed! 🐙

Value of the sequence a at 3.

@[category test, AMS 11] theorem a_3 : a 3 = -24 := ⊢ a 3 = -24 All goals completed! 🐙

Value of the sequence a at 4.

@[category test, AMS 11] theorem a_4 : a 4 = 99 := ⊢ a 4 = 99 All goals completed! 🐙

For all $n \ge 0$, we have $a(2n) = - c(2n+1)$.

k:ℕih1:a (2 * k) = -c (2 * k + 1)ih2:a (2 * (k + 1)) = -c (2 * (k + 1) + 1)h_eq:2 * (k + 2) = 2 * k + 4h_eq2:2 * (k + 2) + 1 = 2 * k + 5h_lhs:a (2 * k + 4) = -6 * a (2 * k + 2) - a (2 * k)h_rhs:c (2 * k + 5) = -6 * c (2 * k + 3) - c (2 * k + 1)ih2':a (2 * k + 2) = -c (2 * k + 3)⊢ -6 * -c (2 * k + 3) - -c (2 * k + 1) = -(-6 * c (2 * k + 3) - c (2 * k + 1)) All goals completed! 🐙

For all $n \ge 0$, we have $a(2n+1) = d(2n+1)$.

All goals completed! 🐙

Conjecture from Creighton Dement (A100434): Let the auxiliary sequences c, d, e, f, g, b be defined as specified. Then for all $n \ge 0$, $c(n) + d(n) = b(n)$.

Proof outline: strong two-step induction on the paired recurrences. The even/odd cases are coupled through closed identities between consecutive terms of the relevant pair of sequences (here $c, d$), and the induction step is discharged by rfl-level unfolding of the definitions plus linear arithmetic. (Numerically verified for $n < 600$ before formalization.)

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/chy4pro/formal-conjectures/blob/32f88077a444b83741f1db6734390eebd3678ecf/FormalConjectures/OEIS/100434.lean#L287"] theorem conjecture1 (n : ℕ) : c n + d n = b n := n:ℕ⊢ c n + d n = b n All goals completed! 🐙

Conjecture from Creighton Dement (A100434): Let the auxiliary sequences c, d, e, f, g, b be defined as specified. Then for all $n \ge 0$, $e(n) + f(n) = b(n)$.

Proof outline: strong two-step induction on the paired recurrences. The even/odd cases are coupled through closed identities between consecutive terms of the relevant pair of sequences (here $e, f$), and the induction step is discharged by rfl-level unfolding of the definitions plus linear arithmetic. (Numerically verified for $n < 600$ before formalization.)

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/chy4pro/formal-conjectures/blob/32f88077a444b83741f1db6734390eebd3678ecf/FormalConjectures/OEIS/100434.lean#L306"] theorem conjecture2 (n : ℕ) : e n + f n = b n := n:ℕ⊢ e n + f n = b n All goals completed! 🐙

Conjecture from Creighton Dement (A100434): Let the auxiliary sequences c, d, e, f, g, b be defined as specified. Then for all $n \ge 0$, $g(n) + a(n) = b(n)$.

Proof outline: strong two-step induction on the paired recurrences. The even/odd cases are coupled through closed identities between consecutive terms of the relevant pair of sequences (here $g, a$), and the induction step is discharged by rfl-level unfolding of the definitions plus linear arithmetic. (Numerically verified for $n < 600$ before formalization.)

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/chy4pro/formal-conjectures/blob/32f88077a444b83741f1db6734390eebd3678ecf/FormalConjectures/OEIS/100434.lean#L335"] theorem conjecture3 (n : ℕ) : g n + a n = b n := n:ℕ⊢ g n + a n = b n All goals completed! 🐙end OeisA100434