e as Iterator Eigenvalue

e as Iterator Eigenvalue

e as Iterator Eigenvalue

Summary

e as Iterator Eigenvalue

Statement

%
\label{def:e-eigenvalue}
The \textbf{$\nu$-eigenvalue} is the Archimedean limit
of the $\nu$-iterator's scaling factor:
\[
    \boxed{%
    e_\nu
    \;:=\;
    \lim_{k \to \infty}\,
    \Bigl(1 + \frac{1}{p_{k+1}}\Bigr)^{p_{k+1}}
    \;\in\; \mathbb{R}.}
\]
Since $p_{k+1} \to \infty$ as $k \to \infty$,
this is a subsequence of the classical sequence
$(1 + 1/n)^n$.
We define
$e := e_\nu = 2.71828\ldots$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 69
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part05/ch26-e-earned.tex lines 151-169

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Transcendentals.EEarned
• Name: e_factorial_sum_scaled

Dependencies

• Canonical: I.D04, I.D06, II.D14, II.D15

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.