Define e and τ (and basic facts about them)

[sudgy]

Possible roadmap:

For e:

• Develop the theory of power series
• Define the exponential function
• Define e = exp(1)

For τ:

• Develop the theory of power series
• Develop the theory of derivatives
• Define the sine and the cosine
• Use https://math.stackexchange.com/a/635552 to prove the sum identities
• Use cos(a - a) identity to prove the Pythagorean identity (not strictly necessary for τ but nice to have)
• Prove that cos(2) < 0
• Use the IVT to prove cos(x) has a root between 0 and 2
• Define τ = 4 * that root
• Use the sum identities to prove that sin(x) and cos(x) are τ-periodic

[sudgy]

Apparently the last step is a bit more complicated than I thought it would be. Here's a huge expansion on that step:

• Show that sin is positive on [0, 2]
• Because cos'(x) = -sin(x), this means that cos is always decreasing on [0, 2], meaning that τ/4 is the only root on [0, 2]
• cos(τ/4)^2 + sin(τ/4)^2 = 1, so sin(τ/4)^2 = 1, and because τ/4 ∈ [0, 2], sin(τ/4) is positive so sin(τ/4) = 1.
• Use cos(τ/4 + τ/4) identity to get cos(τ/2) = -1
• Use sin(τ/4 + τ/4) identity to get sin(τ/2) = 0
• Use cos(τ/4 + τ/2) identity to get cos(3τ/4) = 0
• Use sin(τ/4 + τ/2) identity to get sin(3τ/4) = -1
• Use cos(τ/2 + τ/2) identity to get cos(τ) = 1
• Use sin(τ/2 + τ/2) identity to get sin(τ) = 0
• Use cos(A + τ) identity to show that cos(A + τ) = cos(A)
• Use sin(A + τ) identity to show that sin(A + τ) = sin(A)
• I don't have the full rigor of this step yet, but you can probably use things like cos(τ/4 - x) to show that each quarter of cos/sin is similar, which you can use to show that cos(x) ≠ = 1 when x ∈ (0, τ), showing that τ is the smallest period of cos(x).