avewright/proofwiki-math huggingface dataset:
Theorem: Recurrence Relation where n+1th Term is A by nth term + B to the n

Let $\sequence {a_n}$ be the sequence defined by the recurrence relation:
:$a_n = \begin {cases} 0 & : n = 0 \\ A a_{n - 1} + B^{n - 1} & : n > 0 \end {cases}$
for numbers $A$ and $B$.
Then the closed form for $\sequence {a_n}$ is given by:
:$a_n = \begin {cases} \dfrac {A^n - B^n} {A - B} & : A \ne B \\ n A^{n - 1} & : A = B \end {cases}$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$a_n = \begin {cases} \dfrac {A^n - B^n} {A - B} & : A \ne B \\ n A^{n - 1} & : A = B \end {cases}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \dfrac {A^0 - B^0} {A - B}
      | r = \dfrac {1 - 1} {A - B}
      | c = 
}}
{{eqn | r = \dfrac 0 {A - B}
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{eqn | r = a_0
      | c = 
}}
{{end-eqn}}
When $A = B$:
{{begin-eqn}}
{{eqn | l = 0 A^{-1}
      | r = 0
      | c = 
}}
{{eqn | r = a_0
      | c = 
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
Theorem: Fibonomial Coefficient is Integer

Let $\dbinom n k_\FF$ be a Fibonomial coefficient.
Then $\dbinom n k_\FF$ is an integer.

Proof:
Recurrence Relation for Fibonomial Coefficients gives:
:$\dbinom n k_\FF = F_{k - 1} \dbinom {n - 1} k_\FF + F_{n - k + 1} \dbinom {n - 1} {k - 1}_\FF$
where $F_{k - 1}$ etc. denote Fibonacci numbers.
It follows that each Fibonomial coefficient is the sum of integers, and so an integer.
{{qed}}
Theorem: Recurrence Relation for Fibonomial Coefficients

:$\dbinom n k_\FF = F_{k - 1} \dbinom {n - 1} k_\FF + F_{n - k + 1} \dbinom {n - 1} {k - 1}_\FF$
where:
:$\dbinom n k_\FF$ denotes a Fibonomial coefficient
:$F_{k - 1}$ etc. denote Fibonacci numbers.

Proof:
{{begin-eqn}}
{{eqn | r = F_{k - 1} \dbinom {n - 1} k_\FF + F_{n - k + 1} \dbinom {n - 1} {k - 1}_\FF
      | o = 
      | c = 
}}
{{eqn | r = F_{k - 1} \dfrac {F_{n - 1} F_{n - 2} \cdots F_{n - k + 1} F_{n - k} } {F_k F_{k - 1} F_{k - 2} F_{k - 3} \cdots F_1} + F_{n - k + 1} \dfrac {F_{n - 1} F_{n - 2} \cdots F_{n - k + 1} } {F_{k - 1} F_{k - 2} F_{k - 3} \cdots F_1}
      | c = {{Defof|Fibonomial Coefficient}}
}}
{{eqn | r = \dfrac {F_{k - 1} F_{n - 1} F_{n - 2} \cdots F_{n - k + 1} F_{n - k} + F_{n - k + 1} F_k F_{n - k + 1} F_{n - 1} F_{n - 2} \cdots F_{n - k + 1} } {F_k F_{k - 1} F_{k - 2} F_{k - 3} \cdots F_1}
      | c = 
}}
{{eqn | r = F_{n - 1} F_{n - 2} \cdots F_{n - k + 1} \dfrac {F_{k - 1} F_{n - k} + F_{n - k + 1} F_k} {F_k F_{k - 1} F_{k - 2} F_{k - 3} \cdots F_1}
      | c = 
}}
{{eqn | r = F_{n - 1} F_{n - 2} \cdots F_{n - k + 1} \dfrac {F_{\left({n - k}\right) + k} } {F_k F_{k - 1} F_{k - 2} F_{k - 3} \cdots F_1}
      | c = Honsberger's Identity: $F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$
}}
{{eqn | r = \dfrac {F_n F_{n - 1} F_{n - 2} \cdots F_{n - k + 1} } {F_k F_{k - 1} F_{k - 2} F_{k - 3} \cdots F_1}
      | c = 
}}
{{eqn | r = \dbinom n k_\FF
      | c = {{Defof|Fibonomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Recurrence Relation for Sequence of mth Powers of Fibonacci Numbers

Let $m \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds \sum_{k \mathop \in \Z} \dbinom m k_\FF \paren {-1}^{\ceiling {\paren {m - k} / 2} } {F_{n + k} }^{m - 1} = 0$
where:
:$\dbinom m k_\FF$ denotes a Fibonomial coefficient
:$F_{n + k}$ denotes the $n + k$th Fibonacci number
:$\ceiling {\, \cdot \,}$ denotes the ceiling function

Proof:
=== Lemma 1 ===
{{:Recurrence Relation for Sequence of mth Powers of Fibonacci Numbers/Lemma 1}}
Theorem: Golden Mean by One Minus Golden Mean equals Minus 1

:$\phi \hat \phi = -1$
where:
:$\phi$ denotes the golden mean
:$\hat \phi := 1 - \phi$

Proof:
{{begin-eqn}}
{{eqn | l = \phi 
      | r = \frac 1 {\phi - 1}
      | c = {{Defof|Golden Mean|index = 3}}
}}
{{eqn | ll= \leadsto
      | l = \phi \paren {\phi - 1}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \phi \paren {1 - \phi}
      | r = -1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \phi \hat \phi
      | r = -1
      | c = by definition
}}
{{end-eqn}}
{{qed}}
Category:Golden Mean
goh1na1de9uid35abt0wden1vkynnjk
Theorem: Fibonacci Number of Even Index by Golden Mean Modulo 1

Let $n \in \Z$ be an integer.
Then:
:$F_{2 n} \phi \bmod 1 = 1 - \phi^{-2 n}$
:$F_n$ denotes the $n$th Fibonacci number
:$\phi$ is the golden mean: $\phi = \dfrac {1 + \sqrt 5} 2$

Proof:
From definition of$\bmod 1$, the statement above is equivalent to the statement:
:$F_{2 n} \phi - 1 + \phi^{-2 n}$ is an integer
We have:
{{begin-eqn}}
{{eqn | l = F_{2 n} \phi - 1 + \phi^{-2 n}
      | r = -1 + F_{2 n + 1} - \hat \phi^{2 n} + \phi^{-2 n}
      | c = Fibonacci Number n+1 Minus Golden Mean by Fibonacci Number n
}}
{{eqn | r = -1 + F_{2 n + 1} - \paren {-1}^{2 n} \phi^{-2 n} + \phi^{-2 n}
      | c = Golden Mean by One Minus Golden Mean equals Minus 1
}}
{{eqn | r = -1 + F_{2 n + 1}
}}
{{end-eqn}}
which is an integer.
Hence the result.
{{qed}}
Theorem: Fibonacci Number of Odd Index by Golden Mean Modulo 1

Let $n \in \Z$ be an integer.
Then:
:$F_{2 n + 1} \phi \bmod 1 = \phi^{-2 n - 1}$
where:
:$F_n$ denotes the $n$th Fibonacci number
:$\phi$ is the golden mean: $\phi = \dfrac {1 + \sqrt 5} 2$

Proof:
From definition of$\bmod 1$, the statement above is equivalent to the statement:
:$F_{2 n + 1} \phi - \phi^{-2 n - 1}$ is an integer
We have:
{{begin-eqn}}
{{eqn | l = \phi^2 - \phi \sqrt 5
      | r = \paren {\frac {1 + \sqrt 5} 2}^2 - \paren {\frac {1 + \sqrt 5} 2} \sqrt 5
}}
{{eqn | r = \frac {6 + 2 \sqrt 5} 4 - \frac {5 + \sqrt 5} 2
}}
{{eqn | r = -1
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = F_{2 n + 1} \phi - \phi^{-2 n - 1}
      | r = \frac {\phi^{2 n + 1} - \paren {-1}^{2 n + 1} \phi^{-2 n - 1} } {\sqrt 5} \phi - \phi^{-2 n - 1}
      | c = Euler-Binet Formula
}}
{{eqn | r = \frac {\phi^{2 n + 2} + \phi^{-2 n} - \phi^{-2 n - 1} \sqrt 5} {\sqrt 5} 
}}
{{eqn | r = \frac {\phi^{2 n + 2} + \phi^{-2 n - 2} \paren {\phi^2 - \phi \sqrt 5} } {\sqrt 5} 
}}
{{eqn | r = \frac {\phi^{2 n + 2} - \phi^{-2 n - 2} } {\sqrt 5}
      | c = as $\phi^2 - \phi \sqrt 5 = -1$
}}
{{eqn | r = \frac {\phi^{2 n + 2} - \paren {-1}^{-2 n - 2} \phi^{-2 n - 2} } {\sqrt 5}
}}
{{eqn | r = F_{2 n + 2}
      | c = Euler-Binet Formula
}}
{{end-eqn}}
which is an integer.
{{qed}}
Theorem: Remainder of Fibonacci Number Divided by Fibonacci Number is Plus or Minus Fibonacci Number

Let $F_n$ and $F_m$ be Fibonacci numbers.
By the Division Theorem, let:
:$F_n = q F_m + r$
where:
:$q \in \Z$
:$r \in \Z: 0 \le r < \size {F_m}$
Then either $r$ or $\size {F_m} - r$, or both, is a Fibonacci number.

Proof:
Follows directly from Residue of Fibonacci Number Modulo Fibonacci Number.
{{qed}}
Theorem: Residue of Fibonacci Number Modulo Fibonacci Number

Let $F_n$ denote the $n$th Fibonacci number.
Let $m, r$ be non-negative integers.
Then:
:<nowiki>$F_{m n + r} \equiv \paren {\begin{cases} F_r & : m \bmod 4 = 0 \\
\paren {-1}^{r + 1} F_{n - r} & : m \bmod 4 = 1 \\
\paren {-1}^n F_r & : m \bmod 4 = 2 \\
\paren {-1}^{r + 1 + n} F_{n - r} & : m \bmod 4 = 3 \end{cases} } \pmod {F_n}$</nowiki>

Proof:
=== Lemma ===
{{:Residue of Fibonacci Number Modulo Fibonacci Number/Lemma}}{{qed|lemma}}
We prove the result for all $r$ by induction on $r$:
For all $r \in \N$, let $\map P r$ be the proposition:
:<nowiki>$F_{m n + r} \equiv \paren {\begin{cases} F_r & : m \bmod 4 = 0 \\
\paren {-1}^{r + 1} F_{n - r} & : m \bmod 4 = 1 \\
\paren {-1}^n F_r & : m \bmod 4 = 2 \\
\paren {-1}^{r + 1 + n} F_{n - r} & : m \bmod 4 = 3 \end{cases} } \pmod {F_n}$</nowiki>
Theorem: Sine of Multiple of Pi by 2 plus i by Natural Logarithm of Golden Mean

Let $z = \dfrac \pi 2 + i \ln \phi$.
Then:
:$\dfrac {\sin n z} {\sin z} = i^{1 - n} F_n$
where:
:$\phi$ denotes the golden mean
:$F_n$ denotes the $n$th Fibonacci number.

Proof:
{{begin-eqn}}
{{eqn | l = \sin n z
      | r = \map \sin {\dfrac {n \pi} 2 + i n \ln \phi}
      | c = 
}}
{{eqn | r = \frac {e^{i \paren {\paren {n \pi / 2} + i n \ln \phi} } - e^{-i \paren {\paren {n \pi / 2} + i n \ln \phi} } } {2 i}
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac {e^{i n \pi / 2} e^{-n \ln \phi} - e^{-i n \pi / 2} e^{n \ln \phi} } {2 i}
      | c = 
}}
{{eqn | r = \frac {e^{-n \ln \phi} \paren {\cos \frac {n \pi} 2 + i \sin \frac {n \pi} 2} - e^{n \ln \phi} \paren {\cos \paren {-\frac {n \pi} 2} + i \map \sin {-\frac {n \pi} 2} } } {2 i}
      | c = Euler's Formula and Corollary
}}
{{eqn | r = \frac {e^{-n \ln \phi} \paren {i \sin \frac {n \pi} 2} - e^{n \ln \phi} \paren {i \map \sin {-\frac {n \pi} 2} } } {2 i}
      | c = Cosine of Half-Integer Multiple of Pi
}}
{{eqn | r = \frac {i^n e^{-n \ln \phi} - \paren {-i}^n e^{n \ln \phi} } {2 i}
      | c = Sine of Half-Integer Multiple of Pi and simplification
}}
{{eqn | r = \frac {i^{n - 1} \paren {e^{-n \ln \phi} + e^{n \ln \phi} } } 2
      | c = simplification
}}
{{eqn | r = i^{n - 1} \frac {\phi^n + \frac 1 {\phi^n} } 2
      | c = Exponential of Natural Logarithm
}}
{{eqn | r = i^{n - 1} \frac {\phi^n - \paren {-\frac 1 {\phi^n} } } 2
      | c = 
}}
{{eqn | r = i^{n - 1} \frac {\phi^n - \hat \phi^n} 2
      | c = Reciprocal Form of One Minus Golden Mean
}}
{{end-eqn}}
Setting $n = 1$:
:$\sin z = i^0 \frac {\phi^1 - \hat \phi^1} 2 = \frac {\phi - \hat \phi} 2$
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {\sin n z} {\sin z}
      | r = \dfrac {i^{n - 1} \frac {\phi^n - \hat \phi^n} 2} {\frac {\phi - \hat \phi} 2}
      | c = 
}}
{{eqn | r = i^{n - 1} \dfrac {\phi^n - \hat \phi^n } {\phi - \hat \phi}
      | c = 
}}
{{eqn | r = i^{n - 1} \dfrac {\frac {\phi^n - \hat \phi^n} {\sqrt 5} } {\frac {\phi - \hat \phi} {\sqrt 5} }
      | c = 
}}
{{eqn | r = i^{n - 1} \dfrac {F_n} {F_1}
      | c = Euler-Binet Formula
}}
{{eqn | r = i^{n - 1} F_n
      | c = {{Defof|Fibonacci Number}}: $F_1 = 1$
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Multiple of Pi by 2 plus i by Natural Logarithm of Golden Mean

Let $z = \dfrac \pi 2 + i \ln \phi$.
Then:
:$\dfrac {\sin n z} {\sin z} = i^{1 - n} F_n$
where:
:$\phi$ denotes the golden mean
:$F_n$ denotes the $n$th Fibonacci number.

Proof:
{{begin-eqn}}
{{eqn | l = \cos z
      | r = \map \cos {\dfrac \pi 2 + i \ln \phi}
      | c = 
}}
{{eqn | r = \frac {e^{i \paren {\paren {\pi / 2} + i \ln \phi} } + e^{-i \paren {\paren {\pi / 2} + i \ln \phi} } } 2
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac {e^{i \pi / 2} e^{-\ln \phi} + e^{-i \pi / 2} e^{\ln \phi} } 2
      | c = 
}}
{{eqn | r = \frac {e^{-\ln \phi} \paren {\cos \frac \pi 2 + i \sin \frac \pi 2} + e^{\ln \phi} \paren {\map \cos {-\frac \pi 2} + i \map \sin {-\frac \pi 2} } } 2
      | c = Euler's Formula and {Corollary|Euler's Formula}}
}}
{{eqn | r = \frac {e^{-\ln \phi} \paren {i \sin \frac \pi 2} + e^{\ln \phi} \paren {i \map \sin {-\frac \pi 2} } } 2
      | c = Cosine of Half-Integer Multiple of Pi
}}
{{eqn | r = \frac {i e^{-\ln \phi} - i e^{\ln \phi} } 2
      | c = Sine of Half-Integer Multiple of Pi and simplification
}}
{{eqn | r = -i \frac {\phi - \frac 1 \phi} 2
      | c = Exponential of Natural Logarithm
}}
{{eqn | r = -i \frac {\phi^2 - 1} {2 \phi}
      | c = 
}}
{{eqn | r = -i \frac \phi {2 \phi}
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{eqn | r = \frac {-i} 2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map \sin {n + 1} z + \map \sin {n - 1} z
      | r = 2 \sin n z \cos z
      | c = Werner Formula for Sine by Cosine
}}
{{eqn | r = -i \sin n z
      | c = 
}}
{{end-eqn}}
{{finish|Where to from here?}}
Theorem: Equality of Towers in Set

Let $X$ be a non-empty set.
Let $\struct {T_1, \preccurlyeq_1}$ and $\struct {T_2, \preccurlyeq_2}$ be towers in $X$.
Then either:
:$\struct {T_1, \preccurlyeq_1} = \struct {T_2, \preccurlyeq_2}$
or:
:$\struct {T_1, \preccurlyeq_1}$ is an initial segment of $\struct {T_2, \preccurlyeq_2}$ 
or:
:$\struct {T_2, \preccurlyeq_2}$ is an initial segment of $\struct {T_1, \preccurlyeq_1}$

Proof:
By the definition of tower:
:$\struct {T_1, \preccurlyeq_1}$ and $\struct {T_2, \preccurlyeq_2}$ are well-ordered sets.
By Wosets are Isomorphic to Each Other or Initial Segments, either:
:$(1): \quad$ the towers are order isomorphic to each other
or:
:$(2): \quad$ one is order isomorphic to an initial segment in the other.
{{WLOG}}, in case  $(2)$, assume that $\struct {T_1, \preccurlyeq_1}$ is order isomorphic to an initial segment in $\struct {T_2, \preccurlyeq_2}$.
By Order Isomorphism iff Strictly Increasing Surjection, there exists a strictly increasing mapping:
:$i: \struct {T_1, \preccurlyeq_1} \to \struct {T_2, \preccurlyeq_2}$
such that $i \sqbrk {T_1}$, the image set of $T_1$ under $i$, is equal to $T_2$ or to an initial segment of $T_2$.
From Characterization of Strictly Increasing Mapping on Woset, we can characterize $i$ as follows:
:$\forall t \in T_1: \map i t = \map \min {T_2 \setminus i \sqbrk {S_t} }$
and:
:$i \sqbrk {S_t} = S_{\map i t}$
Define:
:$Y = \set {y \in T_1: \map i y = y}$
Then for any $t \in T_1$ and $S_t \subseteq Y$:
{{begin-eqn}}
{{eqn | l = t
      | r = \map c {X \setminus S_t}
      | c = {{Defof|Tower in Set}}
}}
{{eqn | r = \map c {X \setminus i \sqbrk {S_t} }
      | c = by definition of $Y$
}}
{{eqn | r = \map c {X \setminus S_{\map i t} }
      | c = as $i \sqbrk {S_t} = S_{\map i t}$
}}
{{eqn | r = \map i t
      | c = {{Defof|Tower in Set}}
}}
{{end-eqn}}
So $\map i y = y$ for any initial segment $S_t \subseteq Y$.
By Induction on Well-Ordered Set, $Y = T$.
Thus $i$ is the identity mapping from $T_1$ onto its image.
Recall that the image set of $i$ is $T_2$ or an initial segment of $T_2$.
So $T_1 = T_2$ or an initial segment of $T_2$.
{{qed}}
Theorem: Representations for 1 in Golden Mean Number System

Then there are infinitely many ways to express the number $1$ in the golden mean number system.

Proof:
We have that:
:$\phi^0 = 1$
and so $1$ has the representation $S_1$ as:
:$S_1 := \left[{1 \cdotp 00}\right]_\phi$
By inspection it is seen that $S_1$ is the simplest form of $1$.
Expanding $S_1$:
:$S_2 := \left[{0 \cdotp 11}\right]_\phi$
which can then be expressed as:
:$S_2 := \left[{0 \cdotp 1100}\right]_\phi$
Expanding $S_2$:
:$S_3 := \left[{0 \cdotp 1011}\right]_\phi$
and so:
:$S_4 := \left[{0 \cdotp 101011}\right]_\phi$
Continuing in this way we obtain an infinite sequence $\left\langle{S_n}\right\rangle$ all of which are a representation of $1$.
{{qed}}
Theorem: Golden Mean as Root of Quadratic

The golden mean $\phi$ is one of the roots of the quadratic equation:
:$x^2 - x - 1 = 0$
The other root is $\hat \phi = 1 - \phi$.

Proof:
By Solution to Quadratic Equation:
{{begin-eqn}}
{{eqn | l = x
      | r = \frac {-\paren {-1} \pm \sqrt {\paren {-1}^2 - 4 \times 1 \times \paren {-1} } } {2 \times 1}
      | c = Solution to Quadratic Equation
}}
{{eqn | r = \frac {1 \pm \sqrt 5} 2
      | c = 
}}
{{end-eqn}}
Thus
:$x = \dfrac {1 + \sqrt 5} 2$
and:
:$x = \dfrac {1 - \sqrt 5} 2$
The result follows:
By definition of golden mean:
:$\phi = \dfrac {1 + \sqrt 5} 2$
From Closed Form of One Minus Golden Mean:
:$\hat \phi = 1 - \phi = \dfrac {1 - \sqrt 5} 2$
{{qed}}
Category:Golden Mean
gsq7etrz7hg4rcl00yglw2dby2z28aw
Theorem: Proper Subtower is Initial Segment

Let $\struct {T_1, \preccurlyeq}$ be a proper subtower of $\struct {T_2, \preccurlyeq}$.
Then $\struct {T_1, \preccurlyeq}$ is an initial segment of $\struct {T_2, \preccurlyeq}$.
{{explain|What sort of object is $\struct {T_2, \preccurlyeq}$ -- an ordered set, a totally ordered set, a well-ordered set, an ordinal, what?}}

Proof:
Define the set:
:$Y = \set {y \in T_1: S_y \text { is an initial segment of } \struct {T_2, \preccurlyeq} }$.
Then:
{{begin-eqn}}
{{eqn | l = \map {S_x} {T_1}
      | r = \set {b \in T_1, x \in T_1: b \prec x}
      | c = {{Defof|Initial Segment}}
}}
{{eqn | r = \set {b \in T_2, x \in T_2: b \prec x}
      | c = {{Defof|Proper Subtower in Set}}, as $T_1 \subseteq T_2$
}}
{{eqn | r = \map {S_x} {T_2}
      | c = {{Defof|Initial Segment}}
}}
{{end-eqn}}
By Induction on Well-Ordered Set, $Y = T_1$.
That is, $\struct {T_1, \preccurlyeq}$ is an initial segment in $\struct {T_2, \preccurlyeq}$.
{{qed}}
Theorem: Power of Golden Mean as Sum of Smaller Powers

Let $\phi$ denote the golden mean.
Then:
:$\forall z \in \C: \phi^z = \phi^{z - 1} + \phi^{z - 2}$

Proof:
Let $z \in \C$.
Let $w \in \C$ such that $w + 2 = z$.
Then:
{{begin-eqn}}
{{eqn | l = \phi^z
      | r = \phi^{w + 2}
      | c = 
}}
{{eqn | r = \phi^w \phi^2
      | c = 
}}
{{eqn | r = \phi^w \left({\phi + 1}\right)
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{eqn | r = \phi^{w + 1} + \phi^w
      | c = 
}}
{{eqn | r = \phi^{z - 1} + \phi^{z - 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 100 in Golden Mean Number System is Equivalent to 011

Consider the golden mean number system.
Let $p$ and $q$ be arbitrary strings in $\set {0, 1}$.
Let $x \in \R_{\ge 0}$ have a representation which includes the string $100$, say:
:$x = p100q$
Then $x \in \R_{\ge 0}$ also has the representation:
:$x = p011q$
Similarly, let $x \in \R_{\ge 0}$ have a representation which includes the string $011$, say:
:$x = p011q$
Then $x \in \R_{\ge 0}$ also has the representation:
:$x = p100q$
That is, any instance of $100$ appearing in a representation of a non-negative real number $x$ is equivalent to $011$, and vice versa.
Note that the instance of $100$ or $011$ may also include a radix point; the instance of $011$ or $100$ to which it is equivalent will include the radix point in the same location.

Proof:
Let $100$ appear anywhere within $x$.
Then:
:$x = \phi^r + \ds \sum_{c \mathop \in C} \phi^c$
where:
:$C \subset \Z$
:$r \in \Z$
:$r \notin C, r - 1 \notin C, r - 2 \notin C$
That is, the instance of $100$ corresponds to the indices $r, r - 1, r - 2$.
From Power of Golden Mean as Sum of Smaller Powers:
:$\phi^r = \phi^{r - 1} + \phi^{r - 2}$
and so:
:$x = \phi^{r - 1} + \phi^{r - 2} + \ds \sum_{c \mathop \in C} \phi^c$
That is, the indices instance of $100$ corresponds to the indices $r, r - 1, r - 2$ now correspond to the string $011$.
{{qed}}
Theorem: Conversion of Number in Golden Mean Number System to Simplest Form

Let $x \in \R_{\ge 0}$ have a representation $S$ in the golden mean number system.
Then $S$ can be converted to its simplest form as follows:
:$(1): \quad$ Replace any infinite string on the right hand end of $S$ of the form $010101 \ldots$ with $100$
:$(2): \quad$ Repeatedly replace the leftmost instance of $011$ with $100$.

Proof:
Note that step $(2)$ is an instance of a simplification of $S$.
From 100 in Golden Mean Number System is Equivalent to 011, it has been established that $011$ is equivalent to $100$.
The following need to be established:
:$010101 \ldots$ is equivalent to $100$
:Replacing the leftmost $011$ with $100$ reduces the overall number of instances of $011$.
{{questionable|Except it doesn't, necessarily -- for example it converts $01011$ to $01100$. Something more sophisticated is needed.}}
Let the first $1$ of $010101 \ldots$ represent the instance of $\phi^n$ for some $n \in \Z$.
It follows that the first $0$ of $010101 \ldots$ represents the instance of $\phi^{n + 1}$ for some $n \in \Z$.
Thus $010101 \ldots$ represents the real number $y$ where:
:$y = \phi^n + \phi^{n - 2} + \phi^{n - 4} + \cdots$
and so:
{{begin-eqn}}
{{eqn | l = y
      | r = \phi^n \ds \sum_{k \mathop \ge 0} \phi^{-2 k}
      | c = 
}}
{{eqn | r = \phi^n \dfrac 1 {1 - \phi^{-2} }
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \phi^n \dfrac {\phi^2} {\phi^2 - 1}
      | c = 
}}
{{eqn | r = \phi^n \dfrac {\phi^2} {\paren {\phi + 1} - 1}
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{eqn | r = \phi^{n + 1}
      | c = after simplification
}}
{{end-eqn}}
This can represented in the golden mean number system by $100$, where the $1$ corresponds to the first instance of $\phi^{n + 1}$.
Hence $010101 \ldots$ is equivalent to $100$.
{{qed|lemma}}
{{finish|so far so good, but I'm going to the beach.}}
Theorem: Length of Fibonacci String is Fibonacci Number

Let $S_n$ denote the $n$th Fibonacci string.
Let $\map \len {S_n}$ denote the length of $S_n$.
Then:
:$\map \len {S_n} = F_n$
where $F_n$ denotes the $n$th Fibonacci number.

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\map \len {S_n} = F_n$
Theorem: Incidence of Double Letters in Fibonacci String

Let $S_n$ denote the $n$th Fibonacci string.
Then:
:$(1):\quad$ There are no instances of $2$ $\text a$'s together
:$(2):\quad$ There are no instances of $3$ $\text b$'s together
in $S_n$.

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:There are no instances of $2$ $\text a$'s or $3$ $\text b$'s together in $S_n$.
$\map P 1$ is the case:
:$S_1 = \text a$
Theorem: Fibonacci String Begins with ba

Let $S_n$ be a Fibonacci string of length $n$.
Then for $n \ge 3$, $S_n$ begins with $\text {ba}$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 3}$, let $\map P n$ be the proposition:
:$S_n$ begins with $\text {ba}$
We note in passing that $S_1 = \text a$ and $S_2 = \text b$, so neither of these begin with $\text{ba}$.
Theorem: Fibonacci String Ends with ab or ba

Let $S_n$ be a Fibonacci string of length $n$.
Then for $n \ge 3$, $S_n$ ends either with $\text{ba}$ or with $\text{ab}$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 3}$, let $P \left({n}\right)$ be the proposition:
:$S_n$ ends either with $\text{ba}$ or with $\text{ab}$
We note in passing that $S_1 = \text a$ and $S_2 = \text b$, so neither of these ends either with $\text{ba}$ or with $\text{ab}$.
Theorem: Count of a's and b's in Fibonacci String

Let $S_n$ denote the $n$th Fibonacci string.
Then for $n \ge 3$, $S_n$ has:
:$F_{n - 2}$ instances of $\text a$
:$F_{n - 1}$ instances of $\text b$.

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 3}$, let $\map P n$ be the proposition:
:$S_n$ has $F_{n - 2}$ instances of $\text a$ and $F_{n - 1}$ instances of $\text b$.
Theorem: Prefix of Fibonacci String

Let $n \in \Z_{>1}$.
Let $S_n$ denote the $n$th Fibonacci string.
Let $m \in \Z$ such that $1 < m \le n$.
Let $F_m$ denote the $m$th Fibonacci number.
The prefix of $S_n$ of length $F_m$ is the Fibonacci string $S_m$.

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 3}$, let $\map P n$ be the proposition:
:for all $m \in \Z$ such that $1 < m \le n$, the prefix of $S_n$ of length $F_m$ is $S_m$.
Theorem: Optimal Strategy for Fibonacci Nim

Consider a game of Fibonacci nim with $n$ counters.
Let it be the turn of player $\text A$.
Let the maximum number of counters that can be taken by $\text A$ be $q$.
Let $n$ be expressed in Zeckendorf representation as:
:$n = F_{k_1} + F_{k_2} + \cdots + F_{k_r}$
Then $\text A$ can force a win {{iff}}:
:$F_{k_r} \le q$
and by taking those $F_{k_r}$ counters.

Proof:
{{ProofWanted|working on it, it's fiddly}}
Theorem: Recursively Defined Sequence/Examples/Term is Term of Index less 1 plus 6 times Term of Index less 2

Consider the integer sequence $\left\langle{a_n}\right\rangle$ defined recursively as:
:$a_n = \begin{cases} 0 & : n = 0 \\
1 & : n = 1 \\
a_{n - 1} + 6 a_{n - 2} & : \text{otherwise} \end{cases}$
$a_n$ has a closed-form expression:
:$a_n = \dfrac {3^n - \left({-2}\right)^n} 5$

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $P \left({n}\right)$ be the proposition:
:$a_n = \dfrac {3^n - \left({-2}\right)^n} 5$
Theorem: Recursively Defined Sequence/Examples/Minimum over k of Maximum of 1 plus Function of k and 2 plus Function of n-k

Consider the integer sequence $\sequence {\map f n}$ defined recusrively as:
:<nowiki>$\map f n = \begin{cases} 0 & : n = 1 \\
\ds \min_{0 \mathop < k \mathop < n} \map \max {1 + \map f k, 2 + \map f {n - k} } & : n > 1 \end{cases}$</nowiki>
$\map f n$ has a closed-form expression:
:$\map f n = m$ for $F_m < n \le F_{m + 1}$
where $F_m$ denotes the $m$th Fibonacci number.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$\map f n = m$ for $F_m < n \le F_{m + 1}$