TRIP-Stern sequences

StructureTRIP-Stern tree#✓fully proved

A TRIP-Stern tree with node values in a type \(\alpha\) consists of a root seed in \(\alpha\) together with two maps from \(\alpha\) to \(\alpha\), the left transition and the right transition. No condition is imposed on the seed or on the two transitions; in the source the seed is \((1,1,1)\) and the left and right transitions are induced by the maps \(F_0\) and \(F_1\) defined there.

structure TripSternTree (α : Type _) where
  /-- Distinguished root seed of the tree. Source: Amburg et al., *TRIP-Stern Sequences*, JIS 20
  (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481. -/
  seed : α
  /-- Fixed left transition (induced by `F_0`), taken on a `false` edge.
  Source: Amburg et al., *TRIP-Stern Sequences*, JIS 20 (2017), Article 17.1.7, Definition
  TRIPSternDef, lines 471-481. -/
  leftTransition : α → α
  /-- Fixed right transition (induced by `F_1`), taken on a `true` edge.
  Source: Amburg et al., *TRIP-Stern Sequences*, JIS 20 (2017), Article 17.1.7, Definition
  TRIPSternDef, lines 471-481. -/
  rightTransition : α → α
Sources
  • Ilya Amburg, Krishna Dasaratha, Laure Flapan, Thomas Garrity, Chansoo Lee, Cornelia Mihaila, Nicholas Neumann-Chun, Sarah Peluse, and Matthew Stoffregen, Stern Sequences for a Family of Multidimensional Continued Fractions: TRIP-Stern Sequences, Journal of Integer Sequences 20 (2017), Article 17.1.7, https://cs.uwaterloo.ca/journals/JIS/VOL20/Garrity/garrity6.tex. The tree abstracts Definition TRIPSternDef, lines 471-481 (seed (1,1,1), even/odd recursion by F_0/F_1, levels as index intervals), with F_0/F_1 from line 387; binary paths follow the triangle(v) definition, lines 485-488.
Used by 13
Used byLeft-most node of a TRIP-Stern tree · Recursion for the left-most node · Left-most node at depth zero · The empty path selects the seed · Node selected by a binary path · Extending a path by a left step · Extending a path by a right step · Membership in a level of a TRIP-Stern tree · Nodes at a given depth of a TRIP-Stern tree · Depth zero is the seed · Rightmost node of a TRIP-Stern tree · Successor step of the rightmost node · Rightmost node at depth zero

DefinitionNode selected by a binary path#✓fully proved

Let \(T\) be a TRIP-Stern tree with seed \(s\), left transition \(L\) and right transition \(R\). A binary path is a finite sequence of steps, each left or right. The node of \(T\) selected by a path \((b_1, \dots, b_k)\) is obtained by starting at \(s\) and applying, for \(i = 1, \dots, k\) in order, \(L\) if \(b_i\) is a left step and \(R\) if \(b_i\) is a right step.

def TripSternTree.nodeAtPath {α : Type _} (T : TripSternTree α)
    (path : List Bool) : α :=
  path.foldl (fun node bit =>
    if bit then T.rightTransition node else T.leftTransition node) T.seed
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 1 · Used by 6
Statement usesTRIP-Stern tree
Used byThe empty path selects the seed · Extending a path by a left step · Extending a path by a right step · Membership in a level of a TRIP-Stern tree · Nodes at a given depth of a TRIP-Stern tree · Depth zero is the seed

TheoremThe empty path selects the seed#✓fully proved

For every TRIP-Stern tree \(T\), the node of \(T\) selected by the empty binary path is the seed of \(T\).

theorem TripSternTree.nodeAtEmptyPath {α : Type _} (T : TripSternTree α) :
    T.nodeAtPath [] = T.seed
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2
Statement usesTRIP-Stern tree · Node selected by a binary path

TheoremExtending a path by a left step#✓fully proved

Let \(T\) be a TRIP-Stern tree with left transition \(L\). For every binary path \(p\), the node of \(T\) selected by \(p\) followed by one left step equals \(L\) applied to the node of \(T\) selected by \(p\).

theorem TripSternTree.nodeAtPathAppendLeft {α : Type _}
    (T : TripSternTree α) (path : List Bool) :
    T.nodeAtPath (path ++ [false]) = T.leftTransition (T.nodeAtPath path)
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2
Statement usesTRIP-Stern tree · Node selected by a binary path

TheoremExtending a path by a right step#✓fully proved

Let \(T\) be a TRIP-Stern tree with right transition \(R\). For every binary path \(p\), the node of \(T\) selected by \(p\) followed by one right step equals \(R\) applied to the node of \(T\) selected by \(p\).

theorem TripSternTree.nodeAtPathAppendRight {α : Type _}
    (T : TripSternTree α) (path : List Bool) :
    T.nodeAtPath (path ++ [true]) = T.rightTransition (T.nodeAtPath path)
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2
Statement usesTRIP-Stern tree · Node selected by a binary path

DefinitionNodes at a given depth of a TRIP-Stern tree#✓fully proved

Let \(T\) be a TRIP-Stern tree and \(n\) a natural number. The set of nodes of \(T\) at depth \(n\) is the set of all values \(y\) such that some binary path of length \(n\) selects \(y\) in \(T\).

def TripSternTree.nodesAtDepth {α : Type _} (T : TripSternTree α)
    (n : ℕ) : Set α :=
  { y | ∃ path : List Bool, path.length = n ∧ T.nodeAtPath path = y }
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2 · Used by 2
Statement usesTRIP-Stern tree · Node selected by a binary path
Used byMembership in a level of a TRIP-Stern tree · Depth zero is the seed

TheoremMembership in a level of a TRIP-Stern tree#✓fully proved

For every TRIP-Stern tree \(T\), natural number \(n\) and node value \(y\), \(y\) lies in the set of nodes of \(T\) at depth \(n\) if and only if there is a binary path of length \(n\) whose selected node in \(T\) is \(y\).

theorem TripSternTree.nodeMembershipAtDepth {α : Type _} (T : TripSternTree α)
    (n : ℕ) (y : α) :
    y ∈ T.nodesAtDepth n ↔
      ∃ path : List Bool, path.length = n ∧ T.nodeAtPath path = y
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 3
Statement usesTRIP-Stern tree · Node selected by a binary path · Nodes at a given depth of a TRIP-Stern tree

TheoremDepth zero is the seed#✓fully proved

For every TRIP-Stern tree \(T\) and every node value \(y\), \(y\) lies in the set of nodes of \(T\) at depth \(0\) if and only if \(y\) is the seed of \(T\).

theorem TripSternTree.nodesAtDepthZero {α : Type _}
    (T : TripSternTree α) (y : α) :
    y ∈ T.nodesAtDepth 0 ↔ y = T.seed
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 3
Statement usesTRIP-Stern tree · Nodes at a given depth of a TRIP-Stern tree
Proof usesNode selected by a binary path

DefinitionLeft-most node of a TRIP-Stern tree#✓fully proved

Let \(T\) be a TRIP-Stern tree with seed \(s\) and left transition \(L\). The left-most node of \(T\) at depth \(n\) is \(L^n(s)\), the result of applying \(L\) \(n\) times to \(s\); that is, it is \(s\) at depth \(0\), and at depth \(n + 1\) it is \(L\) applied to the left-most node at depth \(n\).

def TripSternTree.leftmostNode {α : Type _} (T : TripSternTree α) : ℕ → α
  | 0 => T.seed
  | n + 1 => T.leftTransition (T.leftmostNode n)
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 1 · Used by 2
Statement usesTRIP-Stern tree
Used byRecursion for the left-most node · Left-most node at depth zero

DefinitionRightmost node of a TRIP-Stern tree#✓fully proved

For a TRIP-Stern tree \(T\) and a natural number \(n\), the rightmost node of \(T\) at depth \(n\) is obtained from the seed of \(T\) by applying the right transition of \(T\) exactly \(n\) times: at depth \(0\) it is the seed, and at depth \(n + 1\) it is the image of the rightmost node at depth \(n\) under the right transition.

def TripSternTree.rightmostNode {α : Type _} (T : TripSternTree α) : ℕ → α
  | 0 => T.seed
  | n + 1 => T.rightTransition (T.rightmostNode n)
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 1 · Used by 2
Statement usesTRIP-Stern tree
Used bySuccessor step of the rightmost node · Rightmost node at depth zero

TheoremLeft-most node at depth zero#✓fully proved

For every TRIP-Stern tree \(T\), the left-most node of \(T\) at depth \(0\) is the seed of \(T\).

theorem TripSternTree.leftmostNodeAtZero {α : Type _} (T : TripSternTree α) :
    T.leftmostNode 0 = T.seed
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2
Statement usesTRIP-Stern tree · Left-most node of a TRIP-Stern tree

TheoremRecursion for the left-most node#✓fully proved

Let \(T\) be a TRIP-Stern tree with left transition \(L\). For every natural number \(n\), the left-most node of \(T\) at depth \(n + 1\) equals \(L\) applied to the left-most node of \(T\) at depth \(n\).

theorem TripSternTree.leftmostNodeAtSuccessor {α : Type _} (T : TripSternTree α)
    (n : ℕ) :
    T.leftmostNode (n + 1) = T.leftTransition (T.leftmostNode n)
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2
Statement usesTRIP-Stern tree · Left-most node of a TRIP-Stern tree

TheoremRightmost node at depth zero#✓fully proved

For every TRIP-Stern tree \(T\), the rightmost node of \(T\) at depth \(0\) is the seed of \(T\).

theorem TripSternTree.rightmostNodeAtZero {α : Type _} (T : TripSternTree α) :
    T.rightmostNode 0 = T.seed
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2
Statement usesTRIP-Stern tree · Rightmost node of a TRIP-Stern tree

TheoremSuccessor step of the rightmost node#✓fully proved

For every TRIP-Stern tree \(T\) and every natural number \(n\), the rightmost node of \(T\) at depth \(n + 1\) is the image of the rightmost node of \(T\) at depth \(n\) under the right transition of \(T\).

theorem TripSternTree.rightmostNodeAtSuccessor {α : Type _} (T : TripSternTree α)
    (n : ℕ) :
    T.rightmostNode (n + 1) = T.rightTransition (T.rightmostNode n)
Sources
  • Amburg et al., TRIP-Stern Sequences, JIS 20 (2017), Article 17.1.7, Definition TRIPSternDef, lines 471-481.
Uses 2
Statement usesTRIP-Stern tree · Rightmost node of a TRIP-Stern tree
14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.