FormalConjectures/OEIS/112970.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

10 declarations, 4 contain sorry, 0 declared as axioms

A generalized Stern sequence

A112970: A generalized Stern sequence, defined by the recurrence relations: $a(2n+1) = a(n)$ and $a(2n) = a(n) + a(n-2)$ with $a(0)=1$, $a(1)=1$ and $a(n)=0$ for $n \le -1$.

References:

Imports (1)
  1. def OeisA112970.a a n is the generalized Stern sequence, defined by the recurrence relations line 39 source

    Source documentation

    a n is the generalized Stern sequence, defined by the recurrence relations: $a(2n+1) = a(n)$ and $a(2n) = a(n)$ + $a(n-2)$ with $a(0) = 1$, $a(1) = 1$ and $a(n) = 0$ for $n \le -1$.

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Eq, OfNat.ofNat, Not, HDiv.hDiv, HMod.hMod, HSub.hSub, HAdd.hAdd

    15 instances, coercions and auxiliary constants left out.

    def a (n : ℕ) : ℕ :=
…
  2. theorem OeisA112970.a_0 line 55 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Eq, Nat, OeisA112970.a, OfNat.ofNat

    Proof uses: Eq.mpr, ite, HDiv.hDiv, HMod.hMod, LT.lt, HSub.hSub, HAdd.hAdd, id, congrFun', congrArg, OeisA112970.a.eq_def, Eq.refl

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  3. theorem OeisA112970.a_1 line 58 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Eq, Nat, OeisA112970.a, OfNat.ofNat

    Proof uses: Eq.mpr, ite, HDiv.hDiv, HMod.hMod, LT.lt, HSub.hSub, HAdd.hAdd, id, congrFun', congrArg, OeisA112970.a.eq_def, Eq.refl

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  4. theorem OeisA112970.a_2 line 61 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Eq, Nat, OeisA112970.a, OfNat.ofNat

    Proof uses: Eq.mpr, ite, HDiv.hDiv, HMod.hMod, LT.lt, HSub.hSub, HAdd.hAdd, id, congrFun', congrArg, OeisA112970.a.eq_def, ite_congr, Eq.refl, Not, have_body_congr', have_congr'

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  5. theorem OeisA112970.a_3 line 64 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Eq, Nat, OeisA112970.a, OfNat.ofNat

    Proof uses: Eq.mpr, ite, HDiv.hDiv, HMod.hMod, LT.lt, HSub.hSub, HAdd.hAdd, id, congrFun', congrArg, OeisA112970.a.eq_def, ite_congr, Eq.refl, Not, have_body_congr', have_congr'

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  6. theorem OeisA112970.a_4 line 67 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Eq, Nat, OeisA112970.a, OfNat.ofNat

    Proof uses: Eq.mpr, ite, HDiv.hDiv, HMod.hMod, LT.lt, HSub.hSub, HAdd.hAdd, id, congrFun', congrArg, OeisA112970.a.eq_def, ite_congr, Eq.refl, Not, have_body_congr', have_congr'

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  7. theorem OeisA112970.conjecture1 sorry line 76 source

    depends on sorry what this means

    Statement uses: Nat, Eq, OeisA112970.a, HPow.hPow, OfNat.ofNat, HAdd.hAdd

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  8. theorem OeisA112970.conjecture1_value Second part of the conjecture, $a(2^n)=\textrm{A033638}(n)=\lfloor n^2 / 4 \rfloor + 1$ sorry line 85 source

    Source documentation

    Second part of the conjecture, $a(2^n)=\textrm{A033638}(n)=\lfloor n^2 / 4 \rfloor + 1$. It holds by induction on $n$, since $a(2^{n+1}) = a(2^n) + a(2^n - 2)$ for $n \ge 1$ and $a(2^m - 2) = \lfloor (m+1)/2 \rfloor$ for $m \ge 1$.

    depends on sorry what this means

    Statement uses: Nat, Eq, OeisA112970.a, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem conjecture1_value (n : ℕ) : a (2^n) = n ^ 2 / 4 + 1 := by
…

    Mentions: OeisA112970.a

  9. theorem OeisA112970.conjecture2 sorry line 95 source

    depends on sorry what this means

    Statement uses: Nat, Eq, OeisA112970.a, HSub.hSub, HPow.hPow, OfNat.ofNat, HMul.hMul

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  10. theorem OeisA112970.conjecture3 sorry line 102 source

    depends on sorry what this means

    Statement uses: Nat, Eq, OeisA112970.a, HSub.hSub, HPow.hPow, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.