LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The formal hyperbolic tangent and artanh series are inverse, with the artanh derivative

Statement

Let $T$ and $A$ be the formal series of The formal hyperbolic tangent series and the even series $x / \tanh x$ . Then in $Q ⟦ \cdot ⟧$ , $T \circ A = z, A \circ T = x,$ so $T$ and $A$ are mutually inverse formal power series; moreover $A^{'} (z) = \frac{1}{1 - z^{2}} = \sum_{j \geq 0} z^{2 j}, T^{'} (x) = 1 - T (x)^{2},$ and $Q (x) = x / T (x)$ has the expansion $Q (x) = 1 + x^{2} / 3 - x^{4} / 45 + O (x^{6})$ .

Facts & Assumptions

Given: The series $T (x) = (\exp x - \exp (- x)) / (\exp x + \exp (- x))$ and $A (z) = \sum_{j \geq 0} z^{2 j + 1} / (2 j + 1)$ of The formal hyperbolic tangent series and the even series $x / \tanh x$ , with $S = T / x$ , $Q = x / T = 1 / S$ .

[F1]

$A (z) = \frac{1}{2} (\log (1 + z) - \log (1 - z))$ holds coefficientwise: the logarithmic series has $\frac{1}{2} ((- 1)^{n - 1} + 1) z^{n} / n$ , which vanishes for even $n$ and equals $z^{2 j + 1} / (2 j + 1)$ for $n = 2 j + 1$ . This is the recorded relation between the two definitions (The formal hyperbolic tangent series and the even series $x / \tanh x$ , Formal $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws).

[F2]

In a commutative $Q$ -algebra, $\exp (u + v) = \exp (u) \exp (v)$ , $\exp$ and $\log$ are mutually inverse, and $(1 + u)^{c} = \exp (c \log (1 + u))$ (Formal $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws).

[F3]

A series $f \in x R ⟦ x ⟧$ has a two-sided compositional inverse if and only if its linear coefficient is a unit, and then that inverse is unique (A zero-constant formal series has a compositional inverse exactly when its linear coefficient is a unit).

[F4]

Composition is associative when the inner series have zero constant coefficient: $(f \circ g) \circ h = f \circ (g \circ h)$ , and $f \circ x = f$ , $x \circ f = f$ (Substitution by a zero-constant series is a ring homomorphism, and composition is associative when both inner series have zero constant coefficient, Composition $f \circ g$ of formal series when the outer series is a polynomial or the inner series has zero constant term).

[F5]

The formal derivative is additive and satisfies the product, power, quotient and chain rules $D (f g) = (D f) g + f D g$ , $D (f^{m}) = m f^{m - 1} D f$ for $m \geq 1$ , $D (f / g) = ((D f) g - f D g) / g^{2}$ for a unit $g$ , and $D (f \circ g) = (D f \circ g) D g$ (Formal differentiation is linear and satisfies product, power, quotient, chain, and coefficient-recovery laws, The formal derivative $D (\sum a_{n} x^{n}) = \sum_{n \geq 1} n a_{n} x^{n - 1}$ ).

[F6]

A series is a unit exactly when its constant coefficient is a unit, and $\sum_{j \geq 0} (- u)^{j}$ is the inverse of $1 + u$ (A formal power series is a unit exactly when its constant coefficient is a unit).

[F7]

Summable families may be regrouped and reindexed, and infinite products of factors $1 + u_{k}$ with ${ord}_{x} (u_{k}) \to + \infty$ may be regrouped (Summable formal families may be regrouped and rearranged, distribute over multiplication, and have well-defined locally finite products).

Proof

technique · direct; exponentiate $A$, compare the defining quotient of $T$, then differentiate and expand

1.1givenF1

The identity $A (z) = \frac{1}{2} (\log (1 + z) - \log (1 - z))$ holds by [F1].

1.2givenF6F7algebra

Expansion of $Q$ : from $\exp (\pm x)$ with coefficients $(\pm 1)^{n} / n!$ (Formal exponential, logarithm, and binomial powers over a commutative $Q$ -algebra), the even and odd parts are $\exp x + \exp (- x) = 2 + x^{2} + x^{4} / 12 + O (x^{6})$ and $\exp x - \exp (- x) = 2 x + x^{3} / 3 + x^{5} / 60 + O (x^{7})$ . Hence $S = T / x = (2 + x^{2} / 3 + x^{4} / 60 + O (x^{6})) / (2 + x^{2} + x^{4} / 12 + O (x^{6})) = (1 + x^{2} / 6 + x^{4} / 120 + O (x^{6})) (1 - x^{2} / 2 + (1 / 4 - 1 / 24) x^{4} + O (x^{6})) = 1 - x^{2} / 3 + 2 x^{4} / 15 + O (x^{6})$ , and inverting this unit by [F6] gives $Q = 1 / S = 1 + x^{2} / 3 + (1 / 9 - 2 / 15) x^{4} + O (x^{6}) = 1 + x^{2} / 3 - x^{4} / 45 + O (x^{6})$ .

2.1step 1.1F2

Exponentiating: by [F2], $\exp (A) = \exp (\frac{1}{2} \log (1 + z)) \exp (- \frac{1}{2} \log (1 - z)) = (1 + z)^{1 / 2} (1 - z)^{- 1 / 2}$ and similarly $\exp (- A) = (1 + z)^{- 1 / 2} (1 - z)^{1 / 2}$ , where the binomial powers are the series of [F2].

2.2step 1.1F5F6F7algebra

Derivative of $A$ : differentiating $A = \frac{1}{2} (\log (1 + z) - \log (1 - z))$ coefficientwise, $D \log (1 + z) = \sum_{n \geq 1} (- 1)^{n - 1} z^{n - 1} = \sum_{j \geq 0} (- z)^{j} = (1 + z)^{- 1}$ and $D \log (1 - z) = - (1 - z)^{- 1}$ by [F5] and [F6], so $A^{'} = \frac{1}{2} ((1 + z)^{- 1} + (1 - z)^{- 1}) = \frac{1}{2} ((1 - z) + (1 + z)) / (1 - z^{2}) = 1 / (1 - z^{2})$ ; and $(1 - z^{2}) \sum_{j \geq 0} z^{2 j} = 1$ coefficientwise, so $1 / (1 - z^{2}) = \sum_{j \geq 0} z^{2 j}$ by uniqueness of inverses in [F6].

3.1step 2.1F2F6

Both $\exp (A)$ and $\exp (- A)$ have constant term $1$ , so the denominator $\exp (A) + \exp (- A)$ has constant term $2$ , a unit of $Q$ ; the quotient defining $T (A)$ is therefore well defined by [F6]. Multiplying numerator and denominator by the unit $(1 + z)^{1 / 2} (1 - z)^{1 / 2}$ turns it into $((1 + z) - (1 - z)) / ((1 + z) + (1 - z)) = 2 z / 2 = z$ , so $T \circ A = z$ .

4.1step 3.1F3F4

The series $T$ has linear coefficient $1$ , a unit of $Q$ , so by [F3] it has a unique two-sided compositional inverse $g$ , with $g \circ T = x = T \circ g$ . Associativity [F4] applied to the inner series $T, A, g$ (all with zero constant term) gives $A = (g \circ T) \circ A = g \circ (T \circ A) = g \circ z = g$ , so $A = g$ and $A \circ T = x$ .

4.2step 3.1F5algebra

Derivative of $T$ : the termwise derivative of $\exp (\pm x)$ is $\pm \exp (\pm x)$ because $D (\sum_{n} (\pm 1)^{n} x^{n} / n!) = \sum_{n \geq 1} (\pm 1)^{n} x^{n - 1} / (n - 1)!$ ; with $N = \exp x - \exp (- x)$ and $D_{0} = \exp x + \exp (- x)$ this gives $N^{'} = D_{0}$ and $D_{0}^{'} = N$ . The quotient rule [F5] applied to $T = N / D_{0}$ (with $D_{0}$ a unit) gives $T^{'} = (N^{'} D_{0} - N D_{0}^{'}) / D_{0}^{2} = (D_{0}^{2} - N^{2}) / D_{0}^{2} = 1 - T^{2}$ .

5.1step 3.1step 1.2step 4.1step 4.2step 2.2∎

Steps 3.1 and 4.1 give $T \circ A = z$ and $A \circ T = x$ ; steps 2.2 and 4.2 give the two derivative formulas; and step 1.2 gives the recorded expansion of $Q = x / T$ . All identities are coefficientwise identities between formal series; the zero series, the case of a single variable, and the degenerate cases $z = 0$ are included as the constant coefficients of the same computations, and no analytic convergence or choice principle is involved.

Depends on

Used by

The coefficient identity [z²ᵏ](z/tanh z)²ᵏ⁺¹=1 for every k Lemma

Cited to discharge well-definedness by The formal hyperbolic tangent series and the even series x/tanh x.

Dependency tree · two levels

24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jacob Lurie, The Hirzebruch Signature Formula (Lecture 25, Harvard Math 287x notes) (standard reference, not scraped)
Tom Weston, An Introduction to Cobordism Theory (lecture notes, Stanford) (standard reference, not scraped)
John Milnor and James Stasheff, Characteristic Classes (re-typeset scan; original pagination) (standard reference, not scraped)