FormalConjectures/OEIS/271591.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

9 declarations, 1 contain sorry, 0 declared as axioms

Maximal run lengths in the second MSB of Tribonacci numbers $T(n)$

The Tribonacci numbers $T_n$ (A000073). $T_0=0, T_1=0, T_2=1$, and $T_n = T_{n-1} + T_{n-2} + T_{n-3}$ for $n \ge 3$.

Second most significant bit of the tribonacci number A000073(n). This is formalized by extracting the bit at position $\lfloor \log_2 T_n \rfloor - 1$.

References:

Imports (1)
  1. def OeisA271591.tribonacci The Tribonacci numbers $T_n$ (A000073) line 46 source

    Source documentation

    The Tribonacci numbers $T_n$ (A000073). $T_0=0, T_1=0, T_2=1$, and $T_n = T_{n-1} + T_{n-2} + T_{n-3}$ for $n \ge 3$.

    no axioms what this means

    Statement uses: Nat

    2 instances, coercions and auxiliary constants left out.

    def tribonacci (n : ℕ) : ℕ :=
…
  2. def OeisA271591.a Second most significant bit of the tribonacci number A000073(n) line 57 source

    Source documentation

    Second most significant bit of the tribonacci number A000073(n). This is formalized by extracting the bit at position $\lfloor \log_2 T_n \rfloor - 1$.

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: OeisA271591.tribonacci, ite, LE.le, OfNat.ofNat, HSub.hSub, Nat.log2, Eq, Bool, Nat.testBit, Bool.true

    6 instances, coercions and auxiliary constants left out.

    def a (n : ℕ) : ℕ :=
…
  3. def OeisA271591.IsMaximalRun line 66 source

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: And, GE.ge, OfNat.ofNat, LT.lt, Eq, OeisA271591.a, HAdd.hAdd, Ne, HSub.hSub

    7 instances, coercions and auxiliary constants left out.

  4. lemma OeisA271591.a_4 line 77 source

    standard axioms: propext what this means

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

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. lemma OeisA271591.a_5 line 80 source

    standard axioms: propext what this means

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

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  6. lemma OeisA271591.a_6 line 83 source

    standard axioms: propext what this means

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

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. lemma OeisA271591.a_7 line 86 source

    standard axioms: propext what this means

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

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma OeisA271591.a_8 line 89 source

    standard axioms: propext what this means

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

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. theorem OeisA271591.maximal_run_lengths sorry line 100 source

    depends on sorry what this means

    Statement uses: And, Nat, OeisA271591.IsMaximalRun, OfNat.ofNat, Or, Eq

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

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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