such closure. For instance, in the case of $n=8$ (as depicted in
Figure <ref>), it is observed that only a still
acceptable $30.2\%$ of  inversions yield exact results.

scaled y ticks=base 10:-2,
extra y ticks=500,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.002929866,0.007812500,
extra x tick labels=,$0.3\%$,$0.8\%$,
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.92,0.82),anchor=north east,

[characteristic,thick] table [col sep=comma]out/inv-takum16.csv;
[sign] table [col sep=comma]out/inv-posit16.csv;
[direction,densely dashed] table [col sep=comma]out/inv-bfloat16.csv;

Inversion closure analysis of  versus
and  within 's positive dynamic range
$\left[2^{-56},2^{56}\right] \approx [\num{1.4e-17},\num{7.2e16}]$.

Here we observe that extending to $n=16$ bits (see
Figure <ref>) proves advantageous, averting erroneous
conclusions, as in regard to the ratio of exact inversions  drops to a mere
$0.3\%$ at this juncture. Similar findings apply to , with
inversions exhibiting only $0.8\%$ precision, thereby demonstrating a
pronounced advantage for takums, particularly evident for larger values of $n$.

scaled y ticks=base 10:-2,
extra y ticks=30,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.2063492,0.5875000,
extra x tick labels=$20.6\%$,$58.8\%$,
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.08,0.18),anchor=south west,

[characteristic,thick] table [col sep=comma]out/sqrt-takum8.csv;
[sign] table [col sep=comma]out/sqrt-posit8.csv;

Square root closure analysis of  versus
within 's positive dynamic range
$\left[2^{-24},2^{24}\right] \approx [\num{6.0e-8},\num{1.7e7}]$.

Another ubiquitous unary operation is the calculation of the square root, as
illustrated for $n=8$ in Figure <ref>. With
, approximately $58.8\%$ of square roots yield exact results,
contrasting sharply with the mere $20.6\%$ precision achieved by

scaled y ticks=base 10:-2,
extra y ticks=500,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.01269609,0.03125000,0.8409001,
extra x tick labels=,$1.3\%$,$3.1\%$ ,$84.1\%$,
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.7,0.7),anchor=north east,

[characteristic,thick] table [col sep=comma]out/sqrt-takum16.csv;
[sign] table [col sep=comma]out/sqrt-posit16.csv;
[direction,densely dashed] table [col

Square root closure analysis of  versus
and  within 's positive dynamic range
$\left[2^{-56},2^{56}\right] \approx [\num{1.4e-17},\num{7.2e16}]$.

Even though this may appear to present a favourable ratio for ,
upon scrutinising $n=16$ bits (refer to Figure <ref>),
it becomes evident that the exactness rate of  diminishes to
$1.3\%$, with  faring only marginally better at $3.1\%$. In
contrast,  achieves a square root exactness rate of $84.1\%$
without sacrificing precision in non-exact instances. These promising outcomes
are further substantiated by the analysis of the squaring operation, as
depicted in Figures <ref> and
<ref> in the appendix.
Overall, it is imperative for the reader to bear in mind that takums offer an
almost $50\%$ broader dynamic range than  and an even more
substantially broader dynamic range than  and .
Despite this, takums
consistently outperform or match posits and  in all scenarios except
for addition and subtraction. The assessment of the advantage afforded by
takums over posits and  is thus heavily contingent upon the
specific application. Notwithstanding the drawbacks in the realm of addition
and subtraction, the complete closure under inversion and markedly enhanced
exactness in multiplication, division, square root, and squaring tilt the
favour towards takums for general-purpose arithmetic.

§ CONCLUSION

Upon expanding the Gustafson criteria with two supplementary factors
to encompass the desired dynamic range and establish a universally applicable
one, we embarked on an exhaustive exploration of IEEE 754 floating-point
numbers and posits, meticulously scrutinising their performance against these
novel criteria.
The proposed and formally verified takum number format constitutes a
logarithmic bounded-dynamic-range tapered precision number system that fulfils the Gustafson and
newly proposed dynamic range criteria, while demonstrating significantly enhanced
coding efficiency for very high and very small magnitude numbers, and
comparable numerical behaviour to posits. In comparison to posits, takums
exhibit a constant dynamic range for all $n \ge 12$, with the characteristic length
always bounded to $11$ bits, ensuring $n-12$ mantissa bits in all cases. These
improvements are attributed to the absence of reliance on prefix codes, the
bit-optimal leveraging of the unique properties of the number $255$, and
efficient utilisation of implicit bits for the characteristic bits. In essence,
choosing a takum bit string length beyond $12$ bits is solely driven by the
pursuit of desired accuracy, rather than being a joint consideration of
desired accuracy and dynamic range, as is the case with all other existing
number formats.
Based on the tapered format we have explored, we proposed the initiation of a potential new field termed tapered precision numerical analysis
as opposed to the established uniform precision numerical analysis.
Regarding IEEE 754 floating-point numbers, the evaluation reveals that takums
surpass the insufficient dynamic range of the $16$ and $32$ bit formats,
offering significantly more precision for small exponents and only marginally
reduced precision for larger exponents. Takums outperform  by
providing an overall lower relative approximation error and offering up to almost 8
binary orders of magnitude less relative approximation error.
A hardware implementation of takums benefits from the fact that the total characteristic bit count
never exceeds 11 bits, allowing genuine flexibility in precision and sharing of
components for all precisions. Additionally, the lossless convertibility from
64-bit IEEE 754 floating-point numbers to  provides an
efficient pathway for transitioning towards a true mixed-precision workflow in
high-performance computing. The selection of base $\euler$, when coupled with the constrained dynamic range, unveils novel opportunities for hardware arithmetic implementations.
In essence, we have beaten posits at their own game. While upholding all of
Gustafson's criteria, we have matched or even exceeded the original
format in nearly all aspects, ultimately presenting a format that can be used
both for low-precision applications and general-purpose computing.

§ SUPPLEMENTARY CLOSURE ANALYSIS

scale only axis,

scale only axis,

sorted relative precisions

scaled y ticks=base 10:-2,
extra y ticks=500,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.0189024,0.1587302,
extra x tick labels=$1.9\%$,$15.9\%$,
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.92,0.82),anchor=north east,

[characteristic,thick] table
[col sep=comma]out/sub-takum8.csv;
[sign] table [col sep=comma]out/sub-posit8.csv;

Subtraction closure analysis of  versus
within 's positive dynamic range
$\left[2^{-24},2^{24}\right] \approx [\num{6.0e-8},\num{1.7e7}]$.

scale only axis,

scale only axis,

scale only axis,

sorted relative precisions

scaled y ticks=base 10:-2,
extra y ticks=500,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.0,0.03499990,0.1670000,
extra x tick labels=
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.92,0.82),anchor=north east,

[characteristic,thick] table [col
[sign] table [col sep=comma]out/sub-posit16.csv;
[direction,densely dashed] table [col sep=comma]out/sub-bfloat16.csv;

Subtraction closure analysis of  versus
within 's positive dynamic range
$\left[2^{-56},2^{56}\right] \approx [\num{1.4e-17},\num{7.2e16}]$.

scale only axis,

scale only axis,

sorted relative precisions

scaled y ticks=base 10:-2,
extra y ticks=30,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.2559524,0.4033537,
extra x tick labels=$25.6\%$,$40.3\%$,
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.92,0.82),anchor=north east,

[characteristic,thick] table [col sep=comma]out/div-takum8.csv;
[sign] table [col sep=comma]out/div-posit8.csv;

Division closure analysis of  versus
within 's positive dynamic range
$\left[2^{-24},2^{24}\right] \approx [\num{6.0e-8},\num{1.7e7}]$.

scale only axis,

scale only axis,

scale only axis,

sorted relative precisions

scaled y ticks=base 10:-2,
extra y ticks=500,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.02699993,0.03299999,0.3669997,
extra x tick labels=
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.92,0.82),anchor=north east,

[characteristic,thick] table [col
[sign] table [col sep=comma]out/div-posit16.csv;
[direction,densely dashed] table [col sep=comma]out/div-bfloat16.csv;

Division closure analysis of  versus
within 's positive dynamic range
$\left[2^{-56},2^{56}\right] \approx [\num{1.4e-17},\num{7.2e16}]$.

scaled y ticks=base 10:-2,
extra y ticks=500,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.2063492,0.6,
extra x tick labels=$20.6\%$,$60.0\%$,
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.08,0.18),anchor=south west,

[characteristic,thick] table [col
[sign] table [col sep=comma]out/pow2-posit8.csv;

Squaring closure analysis of  versus
within 's positive dynamic range
$\left[2^{-24},2^{24}\right] \approx [\num{6.0e-8},\num{1.7e7}]$.

scaled y ticks=base 10:-2,
extra y ticks=500,
extra y tick labels=$\infty$,

scale only axis,
extra x ticks=0.01269609,0.06250000,
extra x tick labels=    $1.3\%$,$6.3\%$,,
extra x tick style=
ticklabel pos=upper,
point meta=x*100,
legend style=nodes=scale=0.75, transform shape,
legend style=at=(0.92,0.82),anchor=north east,

[characteristic,thick] table [col
[sign] table [col sep=comma]out/pow2-posit16.csv;
[direction,densely dashed] table [col sep=comma]out/pow2-bfloat16.csv;

Squaring closure analysis of  versus
and  within 's positive dynamic range
$\left[2^{-56},2^{56}\right] \approx [\num{1.4e-17},\num{7.2e16}]$.

§ PROOF OF PROPOSITION <REF>: IEEE WASTE RATIO

The number of wasted $\mathrm{NaN}$ bit strings is given by $2^{1+n_f}-3$.
This is because we vary the sign bit and all fraction bits but subtract the two
cases for $\pm\infty$ (where all fraction bits are zero) and a single
$\mathrm{NaN}$ representation that are not redundant.
It holds $\log_2\!\left(\euler^{\pm255}\right) \approx \pm 183.94$. To keep the following derivation
simple and not put IEEE 754 floating-point numbers at a disadvantage, we assume
a simplified slightly
larger desired
dynamic range of $\pm\left(2^{-184},2^{184}\right)$. There are $2^{n_f+1}$
subnormal numbers, which are considered to be in excess when the format flushes
subnormals to zero or when the subnormals are outside the dynamic range
(i.e., when the subnormal exponent $-2^{n_e-1}+1$ is smaller than $-184$,
which is only the case when $n_e \ge 9$).
Left to quantify are the normal bit representations exceeding $2^{-184}$
and $2^{184}$, respectively.
The smallest normal exponent is $-2^{n_e-1}+2$,
meaning there are $\max(0,-184 - (-2^{n_e-1}+2)) = \max(0,2^{n_e-1} - 186)$
excessive exponents at the lower end of the dynamic range.
the largest exponent is $2^{n_e-1}-1$, and
there are $\max(0,2^{n_e-1}-1-183)=\max(0,2^{n_e-1}-184)$ excessive
exponents at the higher end of the
dynamic range (we only go up to exponent $183$ as the significand contained in
$[1,2)$ asymptotically realizes the full quantity $2^{184}$). For each
excessive exponent,
we vary the sign and fraction bits,
adding up to $2^{1+n_f}$ combinations each. Additionally, the maxima can be
omitted when $n_e \ge 9$. In total, we obtain the total number of excessive
bit strings exceeding the dynamic range as $(2^{n_e}-370) \cdot 2^{1+n_f}$
$n_e \ge 9$. The complete expression for all excessive bit strings is:

\begin{equation}
\left[1 + (n_e \ge 9) \cdot (2^{n_e} - 370) + (n_e \ge 9 \lor \text{no
subnormals}) \right] \cdot 2^{1+n_f}-3.
\end{equation}

For the ratio, we divide this expression by the number of bit strings,
$2^{1+n_e+n_f}$, and obtain

\begin{multline}
\left[1 + (n_e \ge 9) \cdot (2^{n_e} - 370) + (n_e \ge 9 \lor \text{no
subnormals}) \right] \cdot 2^{-n_e}-\\
3 \cdot 2^{-1-n_e-n_f},
\end{multline}

which was to be shown.

§ PROOF OF PROPOSITION <REF>: POSIT WASTE RATIO

It holds $\log_2\!\left(\euler^{\pm255}\right) = \pm 183.94$. To keep the following derivation
simple and not put posits at a disadvantage, we assume a simplified slightly
larger desired dynamic range of $\pm\left(2^{-184},2^{184}\right)$.
loss of generality, owing to the symmetry, we can easily determine the number
of excessive bit representations for $\textcolor{p-sign}{S}=0$ and
$\textcolor{p-regime}{R}_0 = 1$, denoting the quadrant with $p \ge 1$, and
multiply it by four. The initial excessive $n$-bit posit value, $2^{184}$, with
$r=46$ and thus $k=47$, results in the binary representation
(the regime consists of 47 ones, and the regime termination bit is a ghost bit
for $n=48$). Leveraging the monotonicity property, we only need to ascertain
the number of representations between this bit string and
$\textcolor{p-sign}{0}\textcolor{p-regime}{1\dots1}$, which corresponds to the
degrees of freedom of $n-48$ bits. This amounts to $2^{n-48}$, multiplied by
four to calculate the total number of excessive representations. The ratio is
determined by dividing this by the total number of posits:

\begin{equation}
\begin{cases}
0 & n \le 47\\
\frac{4 \cdot 2^{n-48}}{2^n} & n \ge 48
\end{cases} =
\begin{cases}
0 & n \le 47\\
2^{-46} & n \ge 48
\end{cases} \approx
\begin{cases}
0 & n \le 47\\
\num{1.42e-14} & n \ge 48.
\end{cases}
\end{equation}

This way we have proven the proposition.

§ PROOF OF PROPOSITION <REF>: TAKUM UNIQUENESS

Let $B =: (\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})$ and
$\tilde{B} =:
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)$.
We can see that the special cases
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) =
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) = \mathrm{NaR}$
and $\takum((\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) =
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) = 0$ immediately
imply $(\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M}) =
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)$ because
they are distinctively defined.
We distinguish all variables of
Definition <ref> in regard to
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}))$ with a
tilde and investigate the last remaining case

\begin{equation}
{(-1)}^{\textcolor{sign}{S}} \euler^\ell =
\takum((\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) =
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) =
{(-1)}^{\textcolor{sign}{\tilde{S}}} \euler^{\tilde{\ell}}.
\end{equation}

This immediately implies $\textcolor{sign}{S} = \textcolor{sign}{\tilde{S}}$
and subsequently $\ell = \tilde{\ell}$, which in turn,
using (<ref>) and $\textcolor{sign}{S} = \textcolor{sign}{\tilde{S}}$,
is equivalent to

\begin{equation}
c + m = \tilde{c} + \tilde{m}.
\end{equation}

Given $c$ and $\tilde{c}$ are integers and
$m,\tilde{m} \in [0,1)$, it directly follows that
$c = \tilde{c}$ and $m=\tilde{m}$.
For $r,\tilde{r} \in \{0,7\}$ the characteristics $c,\tilde{c}$
are contained in the distinct sets
$\{-1\}$, $\{ -3,-2 \}$,
$\{ -7,\dots,-4 \}$, $\{ -15,\dots,-8 \}$, $\{ -31,\dots,-16 \}$,
$\{ -63,\dots,-32 \}$, $\{ -127,\dots,-64 \}$ and
$\{ -255,\dots,-128 \}$ for $\textcolor{direction}{D} = 0$.
Likewise the characteristics $c,\tilde{c}$ are contained in the
distinct sets $\{0\}$, $\{ 1,2 \}$,
$\{ 3,\dots,6 \}$, $\{ 7,\dots,14 \}$, $\{ 15,\dots,30 \}$,
$\{ 31,\dots,62 \}$, $\{ 63,\dots,126 \}$ and
$\{ 127,\dots,254 \}$ for $\textcolor{direction}{D} = 1$.
This means that for the equality
$c=\tilde{c}$ to be satisfied $r=\tilde{r}$ and
$\textcolor{direction}{D} = \textcolor{direction}{\tilde{D}}$
must hold, and thus $\textcolor{regime}{R} = \textcolor{regime}{\tilde{R}}$
and $\textcolor{characteristic}{C} = \textcolor{characteristic}{\tilde{C}}$.
With $r=\tilde{r}$ we can also conclude $p=\tilde{p}$ and
thus, with $m=\tilde{m}$, deduce the equality
$\textcolor{mantissa}{M} = \textcolor{mantissa}{\tilde{M}}$.

§ PROOF OF PROPOSITION <REF>: TAKUM MONOTONICITY

Given $B,\tilde{B} \neq (1,0,\dots,0)$ it follows that
$\takum(B),\takum\!\left(\tilde{B}\right) \neq \mathrm{NaR}$, which in turn means
that $\takum(B),\takum\!\left(\tilde{B}\right) \in \mathbb{R}$. Given
$(\mathbb{R},\le)$ is a partially ordered set, the proposition is
We prove the proposition by proving the equivalent statement

\begin{equation}
\takum(B) < \takum(B+1)
\end{equation}

for $B,B+1 \neq (1,0,\dots,0)$. Let $B =:
\textcolor{characteristic}{C},\textcolor{mantissa}{M})$ and
$B + 1 =:
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)$.
We add a tilde to all corresponding variables of Definition <ref>
in all subsequent cases.
A primary challenge encountered in this proof is the phenomenon whereby incrementing a bit string may precipitate carries that propagate across the full width of the string. Consequently, our strategy entails a detailed examination of all conceivable scenarios wherein segments towards the string's end become sequentially saturated. This approach enables us to identify the specific portions of the bit string that are impacted, thereby facilitating a comprehensive proof of monotonicity.
We employ the notation $\bm{1}$ to denote a bit string comprised entirely of ones, a convention that is slightly extended to accommodate the inclusion of empty bit strings in the context of the characteristic and fraction bits $\textcolor{characteristic}{C}$ and $\textcolor{mantissa}{M}$. This allowance is justified on the grounds that an empty bit string effectively mirrors the external behaviour of a fully ones-populated string: An incrementation transforms an empty string of all ones to an equally empty string of all zeros, seamlessly propagating any incoming carries. Notably, such a configuration precludes the activation of case 5 by an empty $\textcolor{characteristic}{C}$, and similarly, case 6 remains untriggered by an empty $\textcolor{mantissa}{M}$, given that an empty bit string equates to an empty string of all ones.

Case 1 ($\textcolor{sign}{S} = \textcolor{direction}{D} = 1,
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{1}$):
It holds

\begin{align}
\takum\!\left((\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})\right)
&= \takum\!\left((\textcolor{sign}{1},
\textcolor{direction}{1},
\textcolor{regime}{\bm{1}},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}})\right)= -\euler^\ell < 0,\\
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right)
&= \takum\!\left((\textcolor{sign}{0},
\textcolor{direction}{0},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}})\right) = 0,
\end{align}

and thus
\textcolor{characteristic}{C},\textcolor{mantissa}{M})\right) <
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right)$.

Case 2 ($\textcolor{sign}{S} \neq 1, \textcolor{direction}{D} =
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{1}$):
$\textcolor{sign}{S} \neq 1$ directly implies
$\textcolor{sign}{S} = 0$ and it holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{0},
\textcolor{direction}{1},
\textcolor{regime}{\bm{1}},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{1},
\textcolor{direction}{0},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),
\end{align}

however the latter equation is in violation of our precondition,
as we assumed $B + 1 =
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
\neq (1,0,\dots,0)$. This means that we can ignore this case.

In order to streamline the analysis of subsequent cases, all of which conform to the condition $\textcolor{sign}{S} = \textcolor{sign}{\tilde{S}}$, we embark on an examination of the requisite criteria to be met when $\textcolor{sign}{S} = \textcolor{sign}{\tilde{S}}$.
Under the additional assumption
\textcolor{characteristic}{C},\textcolor{mantissa}{M})$,
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right) \neq
\bm{0}$ it holds

\begin{align}
\takum(B) < \takum(B+1)
&\iff {(-1)}^{\textcolor{sign}{S}} \euler^\ell <
{(-1)}^{\textcolor{sign}{S}} \euler^{\tilde{\ell}}\\
&\iff \begin{cases}
\euler^\ell < \euler^{\tilde{\ell}} & \textcolor{sign}{S} = 0\\
-\euler^\ell < -\euler^{\tilde{\ell}} & \textcolor{sign}{S} = 1
\end{cases}\\
&\iff \begin{cases}
\euler^\ell < \euler^{\tilde{\ell}} & \textcolor{sign}{S} = 0\\
\euler^\ell > \euler^{\tilde{\ell}} & \textcolor{sign}{S} = 1
\end{cases}
\end{align}

\begin{align}
&\iff \begin{cases}
\ell < \tilde{\ell} & \textcolor{sign}{S} = 0\\
\ell > \tilde{\ell} & \textcolor{sign}{S} = 1
\end{cases}\\
&\iff \begin{cases}
c+m < \tilde{c}+\tilde{m} & \textcolor{sign}{S} = 0\\
-(c+m) > -\left( \tilde{c}+\tilde{m} \right)
& \textcolor{sign}{S} = 1
\end{cases}\\
&\iff \begin{cases}
c+m < \tilde{c}+\tilde{m} & \textcolor{sign}{S} = 0\\
c+m < \tilde{c}+\tilde{m} & \textcolor{sign}{S} = 1
\end{cases}\\
&\iff (c - \tilde{c}) + (m - \tilde{m}) < 0
\label{eq:takum-proof-monotonicity-goal}
\end{align}

Case 3 ($\textcolor{direction}{D} \neq 1,
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{1}$):
$\textcolor{direction}{D} \neq 1$ directly implies
$\textcolor{direction}{D} = 0$ and it holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{0},
\textcolor{regime}{\bm{1}},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{1},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),
\end{align}

which yields $r=\tilde{r}=0$, $c=-1$, $\tilde{c}=0$, $m \in [0,1)$ and $\tilde{m}=0$. Inserting these results into
(<ref>) we obtain

\begin{equation}
(c - \tilde{c}) + (m - \tilde{m}) < 0
\iff
-1 + m < 0
\iff
m < 1,
\end{equation}

which is satisfied as $f \in [0,1)$.

Case 4 ($\textcolor{regime}{R} \neq \bm{1},
\textcolor{characteristic}{C} = \textcolor{mantissa}{M} = \bm{1}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R} + 1,
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),
\end{align}

where it shall be noted that a change in the regime leads to a shift
of the characteristic and mantissa bits. Nevertheless,
given that both segments remain at zero, this shift is rendered

Case 4a ($\textcolor{direction}{D} = 0$):
It follows $r \in \{1,\dots,7\}$ and $\tilde{r} = r - 1$
given $\textcolor{regime}{R} \neq 1$. The characteristic bits
$\textcolor{characteristic}{C}$ are saturated, which yields
$c = -2^{r+1} + 1 + \left( 2^{r} - 1\right) = -2^r$. In
contrast, the characteristic bits
$\textcolor{characteristic}{\tilde{C}}$ are zero, which yields
$\tilde{c} = -2^{\tilde{r}+1} +1 + 0 = -2^{(r-1)+1} + 1 + 0 = -2^{r} + 1$.
The mantissas $m$ and $\tilde{m}$ follow as
$m \in [0,1)$ and $\tilde{m} = 0$ due to the respectively
saturated and zero mantissa bits. It follows

\begin{equation}
c - \tilde{c} = -2^r + 2^{r} - 1 = -1,
\end{equation}

which is inserted into

\begin{equation}
(c - \tilde{c}) + (m - \tilde{m}) < 0
\iff
-1 + m < 0
\iff
m < 1.
\end{equation}

The inequality is satisfied as $m \in [0,1)$.

Case 4b ($\textcolor{direction}{D} = 1$):
It follows $r \in \{0,\dots,6\}$ and $\tilde{r} = r + 1$
given $\textcolor{regime}{R} \neq 1$. The characteristic bits
$\textcolor{characteristic}{C}$ are saturated, which yields
$c = 2^r - 1 + \left( 2^{r} - 1\right) = 2^{r+1}-2$. In
contrast, the characteristic bits
$\textcolor{characteristic}{\tilde{C}}$ are zero, which yields
$\tilde{c} = 2^{\tilde{r}} - 1 + 0 = 2^{r+1} - 1 + 0 = 2^{r+1} - 1$.
The mantissas $m$ and $\tilde{m}$ follow as
$m \in [0,1)$ and $\tilde{m} = 0$ due to the respectively
saturated and zero mantissa bits. It follows

\begin{equation}
c - \tilde{c} = 2^{r+1}-2 - 2^{r+1} + 1 = -1
\end{equation}

which is inserted into

\begin{equation}
(c - \tilde{c}) + (m - \tilde{m}) < 0
\iff
-1 + m < 0
\iff
m < 1.
\end{equation}

The inequality is satisfied as $m \in [0,1)$.

As both sub-cases fulfil (<ref>),
this case also satisfies the desired inequality.

Case 5 ($\textcolor{characteristic}{C} \neq \bm{1},
\textcolor{mantissa}{M} = \bm{1}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C} + 1,
\textcolor{mantissa}{\bm{0}}),
\end{align}

which yields $r = \tilde{r}$ and $\tilde{c} = c + 1$,
as $\textcolor{characteristic}{C} \neq \bm{1}$.
The mantissas $m$ and $\tilde{m}$ follow as
$m \in [0,1)$ and $\tilde{m} = 0$ due to the respectively
saturated and zero mantissa bits. Inserting these results
into (<ref>) it follows

\begin{equation}
(c - \tilde{c}) + (m - \tilde{m}) < 0
\iff
-1 + m < 0
\iff
m < 1,
\end{equation}

which is satisfied as $m \in [0,1)$.

Case 6 ($\textcolor{mantissa}{M} \neq \bm{1}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{M}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{M} + 1),
\end{align}

which yields $r = \tilde{r}$, $c = \tilde{c}$
and $\tilde{m} > m$, as $\textcolor{mantissa}{M} \neq \bm{1}$.
Inserting these results into
(<ref>) it follows

\begin{equation}
(c - \tilde{c}) + (m - \tilde{m}) < 0
\iff
0 + m - \tilde{m} < 0
\iff
m < \tilde{m},
\end{equation}

which is satisfied.

Given that the cases encompass all possible bit strings, we have demonstrated what needed to be shown.

§ PROOF OF PROPOSITION <REF>: TAKUM NEGATION

The challenge inherent in this proof lies in articulating the inversion and incrementation of the input bit string $(\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R}, \textcolor{characteristic}{C},\textcolor{mantissa}{M})$ in a manner that allows for the analysis of its impacts on the underlying number representation. It can be observed that negating and incrementing preserve any consecutive sequence of zero bits at the trailing end, owing to the carry mechanism. Moreover, upon segmentation of the bit string, it becomes apparent that the carry is propagated to the first non-zero segment, which undergoes an increment of 1. As the segment is non-zero, its inversion does not yield a saturated integer, thereby ensuring that the incrementation does not influence any higher-order bit segments.
For this reason, we will examine all potential scenarios involving consecutive zero-segments at the end. The initial non-zero segment is thereby identified as inverted and incremented (without overflow), while any subsequent segments are solely subjected to inversion. It is noteworthy to emphasise the notation, wherein $\bm{0}$ can represent an empty bit string in the context of $\textcolor{characteristic}{C}$ for $r=0$ and $\textcolor{mantissa}{M}$. This allowance is justified by the fact that an empty bit string remains unchanged under both negation and incrementation operations; the negation of an empty bit string remains an empty bit string, and incrementing an empty bit string also results in an empty bit string.

Case 1 ($\textcolor{sign}{S} = \textcolor{direction}{D} = 0,
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{0}$):
It holds

\begin{equation}
\takum\!\left(\left(\overline{\textcolor{sign}{0}},\overline{\textcolor{direction}{0}},
\overline{\textcolor{regime}{\bm{0}}},
\overline{\textcolor{characteristic}{\bm{0}}},
\overline{\textcolor{mantissa}{\bm{0}}}\right)+1\right) =
\takum\!\left(
\textcolor{regime}{\bm{0}},\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}})
\right) = 0 = -0 =
\textcolor{regime}{\bm{0}},\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}})
\right).
\end{equation}

Case 2 ($\textcolor{sign}{S} \neq 0, \textcolor{direction}{D} = 0,
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{0}$):

$\textcolor{sign}{S} \neq 0$ directly implies $\textcolor{sign}{S} = 1$ and
it holds

\begin{equation}
\takum\!\left(\left(\overline{\textcolor{sign}{1}},\overline{\textcolor{direction}{0}},
\overline{\textcolor{regime}{\bm{0}}},
\overline{\textcolor{characteristic}{\bm{0}}},
\overline{\textcolor{mantissa}{\bm{0}}}\right)+1\right) =
\takum\!\left(
\textcolor{regime}{\bm{0}},\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}})
\right) = \mathrm{NaR} =
\takum\!\left(
\textcolor{regime}{\bm{0}},\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}})
\right).
\end{equation}

For ease of notation we define
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
:= \left(\overline{\textcolor{sign}{S}},\overline{\textcolor{direction}{D}},
\overline{\textcolor{regime}{R}},
\overline{\textcolor{characteristic}{C}},
\overline{\textcolor{mantissa}{M}}\right)+1$ and
add a tilde to all corresponding variables of Definition <ref>
in all subsequent cases.
As $0$ and $\mathrm{NaR}$ have already been covered in the previous two
cases, we can as follows assume (using Proposition <ref>)

\begin{equation}
\takum((\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) =
{(-1)}^{\textcolor{sign}{S}} \euler^{\ell}
\end{equation}

\begin{equation}
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) =
{(-1)}^{\textcolor{sign}{\tilde{S}}} \euler^{\tilde{\ell}}.
\end{equation}

The goal to satisfy
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) =
\textcolor{characteristic}{C},\textcolor{mantissa}{M}))$ can be simplified to

\begin{equation}
\textcolor{sign}{\tilde{S}} = \overline{\textcolor{sign}{S}} \land
\ell = \tilde{\ell}.
\end{equation}

Using (<ref>) we can further reduce it to

\begin{equation}
\textcolor{sign}{\tilde{S}} = \overline{\textcolor{sign}{S}} \land
(c + m = -\tilde{c} - \tilde{m}),
\end{equation}

which is equivalent to

\begin{equation}
\textcolor{sign}{\tilde{S}} = \overline{\textcolor{sign}{S}} \land
((c + \tilde{c}) + (m + \tilde{m}) = 0).
\label{eq:proof-takum-negation-goal}
\end{equation}

Case 3 ($\textcolor{direction}{D} \neq 0,
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{0}$):
It holds as $\textcolor{direction}{D} \neq 0$ directly
implies $\textcolor{direction}{D} = 1$

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M}) &=
\textcolor{direction}{1},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right) &=
\left(
\overline{\textcolor{sign}{S}},
\overline{\textcolor{direction}{D}} + 1,
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{M}
\right) =
\textcolor{direction}{1},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),
\end{align}

which yields $\textcolor{sign}{\tilde{S}} = \overline{\textcolor{sign}{S}}$,
$c = \tilde{c} = 0$ and
$m = \tilde{m} = 0$. This trivially satisfies (<ref>)
with $0+0=0$.

Case 4 ($\textcolor{regime}{R} \neq \bm{0},
\textcolor{characteristic}{C} = \textcolor{mantissa}{M} = \bm{0}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M}) &=
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right) &=
\left(
\overline{\textcolor{sign}{S}},
\overline{\textcolor{direction}{D}},
\overline{\textcolor{regime}{R}} + 1,
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}
\right),
\end{align}

which yields $\textcolor{sign}{\tilde{S}} = \overline{\textcolor{sign}{S}}$,
$\textcolor{characteristic}{C} = \textcolor{characteristic}{\tilde{C}} = \bm{0}$ and
$\textcolor{mantissa}{M} = \textcolor{mantissa}{\tilde{M}} = \bm{0}$,
which implies $m = \tilde{m} = 0$.
With $\textcolor{regime}{R} \neq \bm{0}$
it also holds $\overline{\textcolor{regime}{R}} \neq \bm{1}$.

Case 4a ($\textcolor{direction}{D} = 0$):
We know $\textcolor{direction}{\tilde{D}} = 1$,
$r \in \{0,\dots,6\}$ and

\begin{equation}
\tilde{r} =
\unsignedint(\overline{\textcolor{regime}{R}}+1) =
\unsignedint(\overline{\textcolor{regime}{R}}) + 1 =
(7 - \unsignedint(\textcolor{regime}{R})) + 1
(7 - (7-r)) + 1 = r+1.
\end{equation}

Given $\textcolor{characteristic}{C} = \textcolor{characteristic}{\tilde{C}} = \bm{0}$
it thus holds

\begin{align}
c + \tilde{c} &=
\left( -2^{r+1} +1 + 0 \right) +
\left( 2^{\tilde{r}} - 1 + 0 \right)\\
\left( -2^{r+1} +1 + 0 \right) +
\left( 2^{r+1} - 1 + 0 \right)\\
&= 0.
\end{align}

This trivially satisfies (<ref>)
with $0+0=0$.

Case 4b ($\textcolor{direction}{D} = 1$):
We know $\textcolor{direction}{\tilde{D}} = 0$,
$r \in \{1,\dots,7\}$ and

\begin{equation}
\tilde{r} =
7 - \unsignedint(\overline{\textcolor{regime}{R}}+1) =
6 - \unsignedint(\overline{\textcolor{regime}{R}}) =
6 - (7 - r) = r-1.
\end{equation}

Given $\textcolor{characteristic}{C} = \textcolor{characteristic}{\tilde{C}} = \bm{0}$
it thus holds

\begin{align}
c + \tilde{c} &=
\left( 2^r - 1 + 0 \right) +
\left( -2^{\tilde{r}+1} + 1 + 0 \right)\\
\left( 2^r - 1 + 0 \right) +
\left( -2^{r} + 1 + 0 \right)\\
&= 0.
\end{align}

This trivially satisfies (<ref>)
with $0+0=0$.

As both sub-cases fulfil (<ref>),
this case also satisfies the desired inequality.

Case 5 ($\textcolor{characteristic}{C} \neq \bm{0},
\textcolor{mantissa}{M} = \bm{0}$):
We know that $\textcolor{characteristic}{C} \neq 0$ implies $r>0$, which means
that the segment $\textcolor{characteristic}{C}$ has non-zero length, as
it would otherwise neither stop the carry propagation nor be incremented. It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M}) &=
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{\bm{0}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right) &=
\left(
\overline{\textcolor{sign}{S}},
\overline{\textcolor{direction}{D}},
\overline{\textcolor{regime}{R}},
\overline{\textcolor{characteristic}{C}}+1,
\textcolor{mantissa}{\bm{0}}
\right),
\end{align}

which yields $\textcolor{sign}{\tilde{S}} = \overline{\textcolor{sign}{S}}$.
With $\textcolor{direction}{\tilde{D}} = \overline{\textcolor{direction}{D}}$
and $\textcolor{regime}{\tilde{R}} = \overline{\textcolor{regime}{R}}$ we
observe a double inversion (see (<ref>) and
Lemma <ref>):

\begin{equation}
\tilde{r} = 7 - (7 - r) = r.
\end{equation}

Using $\tilde{r}=r$ (operation 1) and $\textcolor{characteristic}{\tilde{C}} =
\overline{\textcolor{characteristic}{C}} + 1$ and Lemma <ref> (operation 2)
we can deduce for the characteristics

\begin{align}
c + \tilde{c} &\overset{1}{=}
(-2^{r+1}+1+2^r-1) + \sum_{i=0}^{r-1} {\textcolor{characteristic}{\tilde{C}}}_i 2^i +
\sum_{i=0}^{r-1} {\textcolor{characteristic}{C}}_i 2^i\\
-2^r + \left[(2^r - 1) - \left(\sum_{i=0}^{r-1}
{\textcolor{characteristic}{C}}_i 2^i \right) + 1 \right] +
\sum_{i=0}^{r-1} {\textcolor{characteristic}{C}}_i 2^i\\
= 0.
\end{align}

Given $\textcolor{mantissa}{M} = \textcolor{mantissa}{\tilde{M}} = \bm{0}$
it holds $m = \tilde{m} = 0$. This trivially satisfies (<ref>)
with $0+0=0$.

Case 6 ($\textcolor{mantissa}{M} \neq \bm{0}$):
We know that $\textcolor{mantissa}{M} \neq 0$ implies $p>0$, which means
that the segment $\textcolor{mantissa}{M}$ has non-zero length, as
it would otherwise neither stop the carry propagation nor be incremented. It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M}) &=
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{M}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right) &=
\left(
\overline{\textcolor{sign}{S}},
\overline{\textcolor{direction}{D}},
\overline{\textcolor{regime}{R}},
\overline{\textcolor{characteristic}{C}},
\overline{\textcolor{mantissa}{M}} + 1
\right),
\end{align}

which yields $\textcolor{sign}{\tilde{S}} = \overline{\textcolor{sign}{S}}$.
With $\textcolor{direction}{\tilde{D}} = \overline{\textcolor{direction}{D}}$
and $\textcolor{regime}{\tilde{R}} = \overline{\textcolor{regime}{R}}$ we
observe a double inversion (see (<ref>) and
Lemma <ref>):

\begin{equation}
\tilde{r} = 7 - (7 - r) = r.
\end{equation}

Using $\tilde{r}=r$ (operation 1) and $\textcolor{characteristic}{\tilde{C}} =\overline{\textcolor{characteristic}{C}}$ and Lemma <ref> (operation 2)
we can deduce for the characteristics

\begin{align}
c + \tilde{c} &\overset{1}{=}
(-2^{r+1}+1+2^r-1) + \sum_{i=0}^{r-1} {\textcolor{characteristic}{\tilde{C}}}_i 2^i +
\sum_{i=0}^{r-1} {\textcolor{characteristic}{C}}_i 2^i\\
-2^r + \left[(2^r - 1) - \left(\sum_{i=0}^{r-1}
{\textcolor{characteristic}{C}}_i 2^i \right) \right] +
\sum_{i=0}^{r-1} {\textcolor{characteristic}{C}}_i 2^i\\
&= -1.
\end{align}

Using $\tilde{p}=p$ (operation 1), which holds because $\tilde{r}=r$, and
$\textcolor{mantissa}{\tilde{M}} =\overline{\textcolor{mantissa}{M}}+1$
and Lemma <ref> (operation 2) we can show
for the mantissa

\begin{align}
\tilde{m} &\overset{1}{=} 2^{-p} \sum_{i=0}^{p-1} {\textcolor{mantissa}{\tilde{M}}}_i 2^i\\
&\overset{2}{=} 2^{-p} \left[
(2^p - 1) - \left(\sum_{i=0}^{p-1} {\textcolor{mantissa}{M}}_i 2^i \right) + 1
\right]\\
&= 1 - 2^{-p} \sum_{i=0}^{p-1} {\textcolor{mantissa}{M}}_i 2^i\\
&= 1 - m,
\end{align}

which is equivalent to

\begin{equation}
m + \tilde{m} = 1.
\end{equation}

In total we obtain for (<ref>)

\begin{equation}
(a + \tilde{a}) + (m + \tilde{m}) = 0 \iff
-1 + 1 = 0 \iff 0=0,
\end{equation}

which concludes that it is satisfied.

Given that the cases encompass all possible bit strings, we have proven what was intended to be shown.

§ PROOF OF LEMMA <REF>: TAKUM

If $\takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R}, \textcolor{characteristic}{C},\textcolor{mantissa}{M})) = 0$
then the inversion of the sign bit directly yields $\mathrm{NaR}$ by
definition. Otherwise we know

\begin{align}
\takum\!\left(\left(\overline{\textcolor{sign}{S}},\textcolor{direction}{D},
\textcolor{regime}{R}, \textcolor{characteristic}{C},\textcolor{mantissa}{M}\right)\right) &=
{(-1)}^{\overline{\textcolor{sign}{S}}} \euler^{{(-1)}^{\overline{\textcolor{sign}{S}}}(c+m)}\\
&= -\frac{1}{{(-1)}^{\textcolor{sign}{S}} \euler^{{(-1)}^{\textcolor{sign}{S}} (c+m) }}\\
&= -\frac{1}{{(-1)}^{\textcolor{sign}{S}} \euler^{\ell}}\\
&= -\frac{1}{\takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R}, \textcolor{characteristic}{C},\textcolor{mantissa}{M}))},
\end{align}

which was to be shown.

§ PROOF OF PROPOSITION <REF>: TAKUM INVERSION

Let $\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right) :=
\left(\overline{\textcolor{sign}{S}},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M}\right)$. With Lemma <ref>
we know that

\begin{equation}
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) =
\begin{cases}
\textcolor{characteristic}{C},\textcolor{mantissa}{M}))} &
\takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) \neq
\mathrm{NaR} & \takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) = 0.\label{eq:proof-takum-inversion-1}
\end{cases}
\end{equation}

Applying Proposition <ref> and inserting (<ref>)
we can derive

\begin{align}
\takum\!\left(\!\left(\overline{\textcolor{sign}{\tilde{S}}},\overline{\textcolor{direction}{\tilde{D}}},
\overline{\textcolor{regime}{\tilde{R}}},
\overline{\textcolor{characteristic}{\tilde{C}}},\overline{\textcolor{mantissa}{\tilde{M}}}\right)
\!+\!1\!\right) &=
\begin{cases}
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) & \!
\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) \!\neq\!
\mathrm{NaR}\\
\mathrm{NaR} & \!\takum\!\left(\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right)\!=\!
\mathrm{NaR}
\end{cases}\\
&= \begin{cases}
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)\right) &
\takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) \neq 0\\
\mathrm{NaR} & \takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) = 0
\end{cases}\\
&= \begin{cases}
\frac{1}{\takum((\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M}))} &
\takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) \neq 0\\
\mathrm{NaR} & \takum((\textcolor{sign}{S},\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) = 0.
\end{cases}
\end{align}

Given by construction

\begin{equation}
\left(\overline{\textcolor{sign}{\tilde{S}}},\overline{\textcolor{direction}{\tilde{D}}},
\overline{\textcolor{regime}{\tilde{R}}},
\overline{\textcolor{characteristic}{\tilde{C}}},\overline{\textcolor{mantissa}{\tilde{M}}}\right)+1 =
\left(\overline{\overline{\textcolor{sign}{S}}},\overline{\textcolor{direction}{D}},
\overline{\textcolor{regime}{R}},
\overline{\textcolor{characteristic}{C}},\overline{\textcolor{mantissa}{M}}\right)+1 =
\left(\textcolor{sign}{S},\overline{\textcolor{direction}{D}},
\overline{\textcolor{regime}{R}}, \overline{\textcolor{characteristic}{C}},
\overline{\textcolor{mantissa}{M}}\right) + 1
\end{equation}

holds we have proven what was to be shown.

§ PROOF OF PROPOSITION <REF>: TAKUM FLOATING-POINT

The following equality must hold:

\begin{equation}
\takum((\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})) = x,
\end{equation}

which is given in all cases, as $x$ is within $t$'s image by
construction. As $x \neq 0$ the equation is equivalent to

\begin{equation}
{(-1)}^s\cdot \euler^{h \ln(2) + \ln(1+f)} =
{(-1)}^s\cdot (1+f) \cdot 2^h = {(-1)}^{\textcolor{sign}{S}} \euler^{\ell}.
\end{equation}

With $\textcolor{sign}{S}=s$ and using Definition <ref> we

\begin{equation}
2 \left( h \ln(2) + \ln(1+f) \right) = h \log_{\euler}(2) + \log_{\euler}(1+f) = \ell = {(-1)}^{\textcolor{sign}{S}} (c+m).
\end{equation}

This yields <ref> with $\ell \in (-255,255)$ and
is equivalent to

\begin{equation}
{(-1)}^{\textcolor{sign}{S}} \ell = c+m.
\end{equation}

Applying the floor function yields

\begin{equation}
c = \left\lfloor {(-1)}^{\textcolor{sign}{S}} \ell \right\rfloor,
\end{equation}

and likewise

\begin{equation}
m = {(-1)}^{\textcolor{sign}{S}} \ell -
\left\lfloor {(-1)}^{\textcolor{sign}{S}} \ell \right\rfloor =
{(-1)}^{\textcolor{sign}{S}} \ell - c.
\end{equation}

We know that $c$ is always negative and positive for
$\textcolor{direction}{D}=0$ and $\textcolor{direction}{D}=1$
respectively. Thus we can
deduce $\textcolor{direction}{D} = c \ge 0$. The next step is to
determine the regime $r$. We take $c$ and insert the definition

\begin{align}
c &= \begin{cases}
-2^{r+1} + 1 + \sum_{i=0}^{r-1} \textcolor{characteristic}{C}_i 2^{i}
& \textcolor{direction}{D} = 0\\
2^r - 1 + \sum_{i=0}^{r-1} \textcolor{characteristic}{C}_i 2^{i}
& \textcolor{direction}{D} = 1\\
\end{cases}\\
&\in \begin{cases}
\{ -2^{r+1}+1,\dots, -2^{r+1} + 1 + (2^r-1) \} &
\textcolor{direction}{D} = 0\\
\{ 2^r-1,\dots, 2^r - 1 + (2^r-1) \} & \textcolor{direction}{D} = 1
\end{cases}\\
&= \begin{cases}
\{ -2^{r+1}+1, \dots, -2^r \} & \textcolor{direction}{D} = 0\\
\{ 2^r-1,\dots, 2^{r+1} - 2 \} & \textcolor{direction}{D} = 1.
\end{cases}
\end{align}

In particular it holds for $\textcolor{direction}{D} = 0$

\begin{equation}
-c \in \{ 2^r,\dots,2^{r+1}-1 \}
\end{equation}

and for $\textcolor{direction}{D} = 1$

\begin{equation}
c+1 \in \{2^r,\dots,2^{r+1}-1\},
\end{equation}

which yields

\begin{equation}
r = \begin{cases}
\lfloor \log_2(-c) \rfloor & \textcolor{direction}{D} = 0\\
\lfloor \log_2(c+1) \rfloor & \textcolor{direction}{D} = 1.
\end{cases}
\end{equation}

The regime bits follow directly as

\begin{equation}
\textcolor{regime}{R} = \begin{cases}
7 -r & \textcolor{direction}{D} = 0\\
r & \textcolor{direction}{D} = 1.
\end{cases}
\end{equation}

The characteristic bits result directly from the definition

\begin{equation}
\textcolor{characteristic}{C} = \begin{cases}
c + 2^{r+1} - 1 & \textcolor{direction}{D} = 0\\
c - 2^r + 1 & \textcolor{direction}{D} = 1.
\end{cases}
\end{equation}

The mantissa bits $\textcolor{mantissa}{M}$ are obtained by
multiplying $m$ with $2^p$, where $p \in \mathbb{N}_0 \cup \{ \infty \}$
is sufficiently large such that $2^p m \in \mathbb{N}_0$,
which might yield infinitely many mantissa bits:

\begin{align}
p &= \inf_{i \in \mathbb{N}_0} \!\left(2^i m \in \mathbb{N}_0\right) \in
\mathbb{N}_0 \cup \{ \infty \},\\
\textcolor{mantissa}{M} &= 2^p m \in {\{0,1\}}^p.
\end{align}

In total we have obtained all bits of the takum representing
the given floating-point value $x$.

§ PROOF OF PROPOSITION <REF>: TAKUM MANTISSA BIT COUNT

Let $X =: (\textcolor{sign}{S},\textcolor{direction}{D},\textcolor{regime}{R},
\textcolor{characteristic}{C},\textcolor{mantissa}{M})$.
With $x \notin \{ 0, \mathrm{NaR} \}$ we know $x$ has the form

\begin{align}
x = {(-1)}^{\textcolor{sign}{S}} \euler^\ell &\implies
|x| = \euler^\ell\\
&\implies \log_{\euler}(|x|) = 2\ln(|x|) = \ell = {(-1)}^{\textcolor{sign}{S}} (c+m)\\
&\implies 2\ln(|x|) \sign(x) = c + m\\
&\implies \lfloor 2\ln(|x|) \sign(x) \rfloor = c.
\end{align}

As $c+m$ is negative for $\textcolor{direction}{D} = 0$ and positive
for $\textcolor{direction}{D} = 1$ we know

\begin{equation}
\textcolor{direction}{D} = (c+m) \ge 0 = 2\ln(|x|) \sign(x) \ge 0 =
\ln(|x|) \sign(x) \ge 0.
\end{equation}

We can also derive

\begin{align}
|c + \textcolor{direction}{D}| &= \left| \begin{cases}
-2^{r+1} + 1 + \sum_{i=0}^{r-1}
\textcolor{characteristic}{C}_i 2^i & \textcolor{direction}{D} = 0\\
2^r -1 + \left(\sum_{i=0}^{r-1}
\textcolor{characteristic}{C}_i 2^i\right) + 1 & \textcolor{direction}{D} = 1
\end{cases} \right|\\
&\in \left| \begin{cases}
\{ -2^{r+1} + 1,\dots,-2^{r+1} + 1 + (2^r - 1) \} & \textcolor{direction}{D} = 0\\
\{ 2^r,\dots,2^r + (2^r - 1) \} & \textcolor{direction}{D} = 1
\end{cases} \right|\\
&= \left| \begin{cases}
\{ -2^{r+1} + 1,\dots,-2^{r} \} & \textcolor{direction}{D} = 0\\
\{ 2^r,\dots,2^{r+1} - 1 \} & \textcolor{direction}{D} = 1
\end{cases} \right|\\
&= \{ 2^r,\dots,2^{r+1} - 1 \}.
\end{align}

It follows directly that

\begin{equation}
r = \left\lfloor \log_2\!\left(\left|c + \textcolor{direction}{D}\right|\right) \right\rfloor,
\end{equation}

and thus

\begin{equation}
r = \left\lfloor \log_2\!\left(\left|
\lfloor 2\ln(|x|) \sign(x) \rfloor +
(\ln(|x|) \sign(x) \ge 0)
\right|\right) \right\rfloor.
\end{equation}

With $p = n - r - 5$ the proposition follows.

§ PROOF OF PROPOSITION <REF>:
TAKUM MANTISSA BIT COUNT LOWER BOUND

Given $x \in \pm(\euler^{-255},\euler^{255})$, we immediately proceed to the final clause in Algorithm <ref>. Let us denote $X := \truncate_n(\takuminv(x))$. Given $n \ge 12$, we ascertain that the truncation solely impacts the mantissa bits, leaving the sign, direction, regime bits, and characteristic bits unaffected. Consequently, the regime $r$ remains unaltered. Hence, the number of mantissa bits is

\begin{multline}
p = n - 5 -
\left\lfloor \log_2\!\left(\left|
\lfloor 2\ln(|x|) \sign(x) \rfloor +
(\ln(|x|) \sign(x) \ge 0)
\right|\right) \right\rfloor
\in\\ \{ n-12,\dots,n-5 \}
\end{multline}

as per Proposition <ref>.
However, $X$ may be subject to incrementation during rounding. The resultant outcomes may vary depending on the markup of the distinct segments, which we will analyse individually on a case-by-case basis as delineated below.
Let us first define

\begin{align}
X &=:
\textcolor{characteristic}{C},\textcolor{mantissa}{M}),\\
X + 1 &=:
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right),
\end{align}

(applying tildes to the corresponding variables from
Definition <ref>) and then check $r$ and $\tilde{r}$ in all cases.
The notation $\bm{1}$ for a bit string composed entirely of ones may seem somewhat unconventional, particularly when considering the allowance for empty bit strings in the case of the characteristic and mantissa bits $\textcolor{characteristic}{C}$ and $\textcolor{mantissa}{M}$. However, this allowance is justifiable, as an empty bit string behaves equivalently to a bit string of all ones in certain contexts: An empty bit string, when interpreted as one of all ones, retains this equivalence upon incrementation, effectively propagating any carries passed to it. Specifically, case 5 would not be triggered by an empty $\textcolor{characteristic}{C}$, and case 6 would not be triggered by an empty $\textcolor{mantissa}{M}$, since an empty bit string is distinct from a bit string of all ones.

Case 1 ($\textcolor{sign}{S} = \textcolor{direction}{D} = 1,
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{1}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{1},
\textcolor{direction}{1},
\textcolor{regime}{\bm{1}},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{0},
\textcolor{direction}{0},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}).
\end{align}

This overflow to zero would be reset during the subsequent saturation step outlined in Algorithm <ref>. Consequently, in this case, the regime value remains unaffected.

Case 2 ($\textcolor{sign}{S} \neq 1, \textcolor{direction}{D} =
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{1}$):
$\textcolor{sign}{S} \neq 1$ directly implies
$\textcolor{sign}{S} = 0$ and it holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{0},
\textcolor{direction}{1},
\textcolor{regime}{\bm{1}},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{1},
\textcolor{direction}{0},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}).
\end{align}

This overflow to $\mathrm{NaR}$ would be reset during the subsequent saturation step outlined in Algorithm <ref>. Consequently, in this case, the regime value remains unaffected.

Case 3 ($\textcolor{direction}{D} \neq 1,
\textcolor{regime}{R} = \textcolor{characteristic}{C} =
\textcolor{mantissa}{M} = \bm{1}$):
$\textcolor{direction}{D} \neq 1$ directly implies
$\textcolor{direction}{D} = 0$ and it holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{0},
\textcolor{regime}{\bm{1}},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{1},
\textcolor{regime}{\bm{0}},
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),
\end{align}

which yields $r=\tilde{r}=0$.

Case 4 ($\textcolor{regime}{R} \neq \bm{1},
\textcolor{characteristic}{C} = \textcolor{mantissa}{M} = \bm{1}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{\bm{1}},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R} + 1,
\textcolor{characteristic}{\bm{0}},
\textcolor{mantissa}{\bm{0}}),
\end{align}

where it shall be noted that a change in the regime leads to a shift
of the characteristic and mantissa bits. However, as both segments are
zero, the shift is inconsequential.

Case 4a ($\textcolor{direction}{D} = 0$):
It follows $r \in \{1,\dots,7\}$ and $\tilde{r} = r - 1$
given $\textcolor{regime}{R} \neq 1$.

Case 4b ($\textcolor{direction}{D} = 1$):
It follows $r \in \{0,\dots,6\}$ and $\tilde{r} = r + 1$
given $\textcolor{regime}{R} \neq 1$.

Case 5 ($\textcolor{characteristic}{C} \neq \bm{1},
\textcolor{mantissa}{M} = \bm{1}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{\bm{1}}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C} + 1,
\textcolor{mantissa}{\bm{0}}),
\end{align}

which yields $r = \tilde{r}$.

Case 6 ($\textcolor{mantissa}{M} \neq \bm{1}$):
It holds

\begin{align}
\textcolor{characteristic}{C},\textcolor{mantissa}{M})
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{M}),\\
\left(\textcolor{sign}{\tilde{S}},\textcolor{direction}{\tilde{D}},
\textcolor{regime}{\tilde{R}},
\textcolor{characteristic}{\tilde{C}},\textcolor{mantissa}{\tilde{M}}\right)
&= (\textcolor{sign}{S},
\textcolor{direction}{D},
\textcolor{regime}{R},
\textcolor{characteristic}{C},
\textcolor{mantissa}{M} + 1),
\end{align}

which yields $r = \tilde{r}$.

As we can see the regime value is only changed in case 4 and
either incremented or decremented depending on $\textcolor{direction}{D}$.
It immediately follows

\begin{equation}
\tilde{p} = \begin{cases}
\begin{cases}
p + 1 & \textcolor{direction}{D} = 0\\
p - 1 & \textcolor{direction}{D} = 1
\end{cases} & \textcolor{regime}{R} \neq \bm{1},
\textcolor{characteristic}{C} = \textcolor{mantissa}{M} = \bm{1}\\
p & \text{otherwise},
\end{cases}
\end{equation}

in particular $\tilde{p} \in \{ p-1, p, p+1 \}$ and thus
$\tilde{p} \ge p-1$, which was to be shown.

§ PROOF OF PROPOSITION <REF>: TAKUM MACHINE

Given $\round(0)=0$ and $x \neq \mathrm{NaR}$ we can assume
$x$ to have the form ${(-1)}^{\textcolor{sign}{S}} \euler^{\tilde{\ell}}$ with
$\tilde{\ell} \in (-255,255)$. The result of the rounding,
$\round(x)$, has the form ${(-1)}^{\textcolor{sign}{S}} \euler^\ell$.
The logarithmic value $\ell \in (-255,255)$ has $p$ mantissa bits and differs at
most by $\pm 2^{-p-1}$ from $\tilde{\ell}$ after rounding. It thus follows with

\begin{equation}
\euler^{2^{-p-1}} - 1 \ge 1 - \euler^{-2^{-p-1}} \iff
\euler^{-2^{-p-1}} {\left(\euler^{2^{-p-1}} - 1\right)}^2 \ge 0,
\end{equation}

which always holds, that

\begin{align}
\left| \frac{x - \round(x)}{x} \right| &=
\left| 1 - \frac{\round(x)}{x} \right|\\
&= \left| 1 - \frac{{(-1)}^{\textcolor{sign}{S}} \euler^\ell}
{{(-1)}^{\textcolor{sign}{S}} \euler^{\tilde{\ell}}} \right|\\
&= \left| 1 - \euler^{\ell - \tilde{\ell}} \right|\\
&\le \max\!\left(
\left| 1 - \euler^{2^{-p-1}} \right|,
\left| 1 - \euler^{-2^{-p-1}} \right|
\right)\\
&= \max\!\left(
\euler^{2^{-p-1}} - 1,
1 - \euler^{-2^{-p-1}}
\right)\\
&= \euler^{2^{-p-1}} - 1\\
&= \lambda(p).
\end{align}

Next we show that $\lambda(p) < \frac{2}{3} \varepsilon(p)$. It holds

\begin{equation}\label{eq:takum-proof-prec-subtraction}
\lambda(p) - \varepsilon(p) = \euler^{2^{-p-1}}- 2^{-p-1} - 1.
\end{equation}

We know that for $z \in (0,0.5)$ the function $\euler^z = \exp\!\left(\frac{z}{2}\right)$
has the Taylor polynomial with Lagrange remainder at $0$

\begin{equation}
\exp\!\left(\frac{z}{2}\right) = 1 + \frac{z}{2} + \frac{\exp''(\xi)}{2!}
{\left(\frac{z}{2}\right)}^2 =
1 + \frac{z}{2} + \frac{\exp(\xi)}{2} {\left(\frac{z}{2}\right)}^2 <
1 + \frac{z}{2} + \frac{\sqrt[4]{\mathrm{e}}}{2} {\left(\frac{z}{2}\right)}^2
\end{equation}

with $\xi \in \left(0,\frac{z}{2}\right) \subset (0,0.25)$, which is equivalent to

\begin{equation}
\exp\!\left(\frac{z}{2}\right) - \frac{z}{2} - 1 < \frac{\sqrt[4]{\mathrm{e}}}{2}
{\left(\frac{z}{2}\right)}^2 \iff
\euler^z - z - 1 < \frac{\sqrt[4]{\mathrm{e}}}{2}
{\left(\frac{z}{2}\right)}^2 - \frac{z}{2}.
\end{equation}

If we look back at (<ref>) we can see that
with $z = 2^{-p-1} = \varepsilon(p) \in (0,0.5)$ and
$\varepsilon^2(p) < \varepsilon(p)$ it holds

\begin{align}
\lambda(p) - \varepsilon(p) = \euler^{2^{-p-1}} - 2^{-p-1} - 1 &< \frac{\sqrt[4]{\mathrm{e}}}{2}
{\left(\frac{\varepsilon(p)}{2}\right)}^2 -
\frac{\varepsilon(p)}{2}\\
&< \frac{\sqrt[4]{\mathrm{e}}}{8}
\varepsilon(p) - \frac{\varepsilon(p)}{2}\\
&= \left( \frac{\sqrt[4]{\mathrm{e}}}{8} - \frac{1}{2} \right)
\varepsilon(p)\\
&\approx -0.339 \cdot \varepsilon(p)\\
&< -\frac{\varepsilon(p)}{3}.
\end{align}

This is equivalent to

\begin{equation}
\lambda(p) < \frac{2}{3} \varepsilon(p),
\end{equation}

which was to be shown.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

New York, NY, USA

Association for Computing Machinery

journaltitleACM Transactions on Architecture and Code Optimization
titleLow-precision Logarithmic Number Systems: Beyond Base-2
family=Che Ismail,

booktitle2020 FORTEI-International Conference on Electrical Engineering (FORTEI-ICEE)
titleAn Investigation of Extended Co-Transformation using Second-Degree Interpolation for Logarithmic Number System

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleThe Origins of Digital Computers: Selected Papers
titlePreliminary Discussion of the Logical Design of an Electronic Computing Instrument

journaltitleMathematical Structures in Computer Science
titleWheels – on division by zero
family=Che Ismail,

journaltitleIEEE Transactions on Computers
titleLNS with Co-Transformation Competes with Floating-Point

journaltitleIEEE Transactions on Computers
titleArithmetic on the European logarithmic microprocessor

Singapore, Singapore

Association for Computing Machinery

titlePosits: The Good, the Bad and the Ugly

titleEvery Bit Counts: Posit Arithmetic

CRC Press

seriesChapman & Hall/CRC Computational Science
titleThe End of Error: Unum Computing

Chelyabinsk, Russia

South Ural State University

journaltitleSupercomputing Frontiers and Innovations
titleBeating Floating Point at Its Own Game: Posit Arithmetic

titleStandard for Posit™ Arithmetic (2022)

journaltitleIEEE Std 754-2019 (Revision of IEEE 754-2008)
titleIEEE Standard for Floating-Point Arithmetic

Los Alamitos, CA, USA

IEEE Computer Society

booktitle2020 IEEE 27th Symposium on Computer Arithmetic (ARITH)
titleEfficient, arbitrarily high precision hardware logarithmic arithmetic for linear algebra

titleRethinking floating point for deep learning

titleLecture Notes on the Status of IEEE Standard 754 for Binary Floating-Point Arithmetic
ive.org/web/20240308034347/https://people.eecs.berkeley.edu/ wkahan/ieee754status/IEEE754.PDF

titleNames for Standardized Floating-Point Formats
ive.org/web/20231227155514/https://people.eecs.berkeley.edu/ wkahan/ieee754status/Names.pdf

titleTensorFloat-32 in the A100 GPU Accelerates AI Training, HPC up to 20x

booktitle2018 7th International Conference on Modern Circuits and Systems Technologies (MOCAST)
titleLogarithmic Number System for Deep Learning

John Wiley & Sons, Ltd

booktitleFundamentals and Applications of Colour Engineering
titleColor on the Web

Singapore, Singapore

Association for Computing Machinery

booktitleProceedings of the Conference for Next Generation Arithmetic
seriesCoNGA '18
titleUniversal Coding of the Reals: Alternatives to IEEE Floating Point

titleConvolutional Neural Networks using Logarithmic Data Representation

journaltitleIEEE Transactions on Computers
titleTapered Floating Point: A New Floating-Point Representation

Los Alamitos, CA, USA

IEEE Computer Society

journaltitleIEEE Transactions on Computers
titleDiscrete Basis and Computation of Elementary Functions

titleAlgorithm-Hardware Co-Design of Distribution-Aware Logarithmic-Posit Encodings for Efficient DNN Inference
family=Torres Quevedo,

Madrid, Spain

journaltitleRevista de Obras Públicas
titleAutomática: Complemento de la Teoría de las Máquinas

titleBFloat16: The secret to high performance on Cloud TPUs