- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
If \(m_1, m_2\) are both odd, \(\geq 3\), satisfy \(m_1 \equiv m_2 \pmod{42}\), and both give \(-2\theta + 1 = \theta ^{m_i} - \theta '^{\, m_i}\), then \(m_1 = m_2\).
Proof sketch: if \(m_1 \neq m_2\), let \(d = |m_2 - m_1|\), which is divisible by \(42\) (hence by \(7\)). The \(7\)-adic analysis of Lemma 29 combined with Corollary C yields a contradiction on the valuation of \(\sqrt{-7} \cdot B_d\).
The conjugate factors are coprime in \(R\). The only prime factors of \(2\) in \(R\) are \(\theta \) and \(\theta '\) (since \(2 = \theta \cdot \theta '\)). If either divided both factors, it would divide their difference \(\sqrt{-7}\), but \(N(\sqrt{-7}) = 7\) is not divisible by \(N(\theta ) = N(\theta ') = 2\).
Any two solutions of the Ramanujan–Nagell equation produce the same theta expression: if \((x_1^2 + 7)/4 = 2^{m_1}\) and \((x_2^2 + 7)/4 = 2^{m_2}\) for odd \(m_1, m_2 \geq 3\), then \(\theta ^{m_1} - \theta '^{\, m_1} = \theta ^{m_2} - \theta '^{\, m_2}\).
From \(\alpha = \pm \theta ^m\) or \(\alpha = \pm \theta '^{\, m}\), use the product relation to determine \(\beta \), then take the difference \(\alpha - \beta = 2\theta - 1\) to eliminate \(x\) and obtain: either \(2\theta - 1 = \theta ^m - \theta '^{\, m}\) or \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\).
From \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\), expand via the binomial theorem and reduce modulo \(7\) to obtain \(-2^{m-1} \equiv m \pmod{7}\).
The proof multiplies both sides by \(2^m\), expands \((1 + \sqrt{-7})^m - (1 - \sqrt{-7})^m\) via the binomial theorem, observes that even-index terms cancel and odd-index terms involve powers of \((\sqrt{-7})^2 = -7\), then reads the result modulo \(7\).
The \(7\)-adic valuation of \(B_d\) equals \(v_7(d)\): if \(7^l \| d\) (i.e. \(7^l \mid d\) but \(7^{l+1} \nmid d\)), then \(7^l \mid B_d\) and \(7^{l+1} \nmid B_d\).
This is the core of the \(7\)-adic analysis: the \(j=0\) term of \(B_d\) equals \(d\), and all higher terms have strictly larger \(7\)-adic valuation.
If either \(2\theta - 1 = \theta ^m - \theta '^{\, m}\) or \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\) holds for odd \(m \geq 3\), then in fact the minus sign must hold: \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\). This is proved by reducing modulo \(\theta '^2\) and checking which sign is consistent.
If \(\alpha \cdot \beta = \theta ^m \cdot \theta '^{\, m}\) and \(\gcd (\alpha , \beta ) = 1\) in the UFD \(R\), then \(\alpha = \pm \theta ^m\) or \(\alpha = \pm \theta '^{\, m}\). This combines unique factorization (class_number_one) with the fact that the only units are \(\pm 1\) (units_pm_one).
If \(n\) is odd with \(n \geq 5\) and \(x^2 + 7 = 2^n\), then \(n \in \{ 5, 7, 15\} \).
From the mod \(42\) constraint, \(m = n - 2\) lies in one of three residue classes (\(3\), \(5\), or \(13\) mod \(42\)). The verification lemmas show these are actual solutions (at \(m = 3, 5, 13\)). The uniqueness lemma shows each residue class has at most one solution. Therefore \(n \in \{ 5, 7, 15\} \).
If \(n\) is odd with \(n \geq 5\) and \(x^2 + 7 = 2^n\), then \((n - 2) \bmod 42 \in \{ 3, 5, 13\} \).
This follows from \((-2)^{n-3} \equiv n - 2 \pmod{7}\) together with Fermat’s little theorem \(2^6 \equiv 1 \pmod{7}\). Checking residues modulo \(42\) (combining mod \(6\) and mod \(7\)) yields the three residue classes.