Elementary b = 2 Ramanujan–Nagell branches

[roed-math]

Goal

The elementary layer of the generalized Ramanujan–Nagell solver for base b = 2: complete congruence/descent proofs for every concrete (D, k) with D odd, D ≢ 7 (mod 8) (the (B)-finisher) and every even D (the (C)-descent), packaged as an exact recursion whose only non-elementary tail is the split configuration D ≡ 7 (mod 8). The tail is routed, not solved, here: after the descent, (D, k) = (7, 1) goes to today's hardwired classical path unchanged, and every other split instance keeps today's typed SolverUnavailable until #86 + #87 land. Evidence for the elementary regimes is Evidence(kind="structural", ...) carrying the congruence/descent argument; completeness="proved".

Every proof in this issue is written out in full below (ground: proved inline, each step elementary; and the resulting solution sets were independently re-verified by exhaustive search on Sage 10.7 — see "Acceptance criteria").

Target base

• Repository state: branch review-architecture @ 85f8e0a (the composed
  tree on the roed-math fork: wave-1 code = PRs Packaging, CI, design notes, and the annotated bibliography #2–Family: waring — Waring-type diagonal representation #48, plus the wave-2 and
  architecture-review series, which are not yet opened as PRs).
• Required merged PRs: Packaging, CI, design notes, and the annotated bibliography #2–Family: waring — Waring-type diagonal representation #48 (wave 1); the wave-2/architecture-review series
  must land after them before this issue's work can merge to main.
  Implementation happens on the composed tree, not on a split branch.

Dependencies

• Parent: Proved completion for the supported generalized Ramanujan–Nagell class (tracking) #75
• Blocked by: none. The layer is implementable today because its non-elementary tail defers: to the existing hardwired (7, 1, 2) fast path, and otherwise to the existing verbatim SolverUnavailable (which Ramanujan–Nagell solver integration and regression fixtures #88 later replaces by the Pethő–de Weger ideal and recurrence branch enumeration #86/Explicit analytic bounds and certified reductions for Ramanujan–Nagell #87 machinery).
• Unblocks: Ramanujan–Nagell solver integration and regression fixtures #88 (which wires this layer into the dispatch).

Supported inputs

Reduced-base instances with b = 2 exactly (#88's perfect-power reduction sends b = 2^e here with the e | N filter; 2 itself is not a perfect power), concrete D >= 1, concrete k >= 1 with k odd (gcd(k, 2) = 1 is enforced upstream by #88's guards); unknowns (x, n) with n >= 0, solutions reported as x >= 0 representatives under the sign symmetry (conventions owned by #88).

Algorithm and conventions

The exact recursion ELEM(D, k)

All case tests are exact integer congruences; "checked directly" means: for each listed n, compute t = k * 2^n - D exactly and accept (ZZ(t).isqrt(), n) iff t >= 0 and ZZ(t).is_square().

1. (B)-finisher — D odd, D ≢ 7 (mod 8). Every solution has n <= 2.
   Proof (complete). Suppose n >= 3, so 8 | k * 2^n. If x is even then x^2 + D is odd (D odd) while k * 2^n is even — impossible. So x is odd, hence x^2 ≡ 1 (mod 8) and x^2 + D ≡ 1 + D (mod 8). Since D ≢ 7 (mod 8), 1 + D ≢ 0 (mod 8), contradicting 8 | x^2 + D. Hence n <= 2. ∎
   Return the direct checks for n ∈ {0, 1, 2}. Proved, structural evidence.

2. (C), D ≡ 2 (mod 4). Every solution has n <= 1.
   Proof. For n >= 2, 4 | k * 2^n, so x^2 ≡ -D ≡ 2 (mod 4) — impossible, squares are 0 or 1 (mod 4). ∎
   Return the direct checks for n ∈ {0, 1}. Proved, structural evidence.

3. (C)-descent, D ≡ 0 (mod 4) (so D >= 4). Direct checks for n ∈ {0, 1}. For n >= 2: x^2 = k * 2^n - D ≡ 0 (mod 4), so x is even; writing x = 2t gives exactly t^2 + D/4 = k * 2^(n-2). Recurse on ELEM(D/4, k) and transport its solution set through the bijection

   (t, n')  <->  (x, n) = (2*t, n' + 2)
   

   (both directions exact and inverse to each other; the direct checks at this level cover n ∈ {0, 1}, the recursion covers n >= 2).
   Termination. v_2(D) drops by exactly 2 per level and D/4 >= 1, so after at most floor(v_2(D)/2) steps the recursion reaches an odd D (case 1 or case 4) or a D ≡ 2 (mod 4) (case 2). ∎
   Proved, structural evidence (the evidence records the full descent chain D -> D/4 -> ...).

4. Split tail — D odd, D ≡ 7 (mod 8). Not elementary; this child only routes it:

   • (D, k) = (7, 1) reached at the top level (no descent applied): return the hardwired classical result unchanged (Nagell 1961 theorem evidence, scope "representatives with x > 0; the full set adds x -> -x" — the existing fast path, byte for byte).
   • (D, k) = (7, 1) reached through the (C)-descent (i.e. the original D was 4^j * 7 for some j >= 1): transport the hardwired solution set through the descent bijection composed j times, i.e. (x, n) = (2^j * t, n' + 2*j), and report it with scope "representatives with x >= 0; the full set adds x -> -x" (the transported set contains no x = 0, so the two scope strings describe the same set here; the layer nonetheless standardizes on the x >= 0 string outside the untouched fast path). Evidence: the Evidence(kind="theorem", reference="Nagell1961", ...) record of the fast path plus the Evidence(kind="structural", ...) record of the descent chain.
   • any other (D, k): until Pethő–de Weger ideal and recurrence branch enumeration #86 + Explicit analytic bounds and certified reductions for Ramanujan–Nagell #87 land, the whole original instance raises today's SolverUnavailable("only the classical x^2 + 7 = 2^n is hardwired; general (d, k, b) need a Baker + LLL computation (Petho-de Weger)", outcome="unsupported-family") — message preserved verbatim. Never return the partial small-n data gathered on the way down: this family has no partial path and this child does not add one. After Pethő–de Weger ideal and recurrence branch enumeration #86/Explicit analytic bounds and certified reductions for Ramanujan–Nagell #87 land, Ramanujan–Nagell solver integration and regression fixtures #88 replaces this deferral by the split machinery; the routing point and its test are defined here so the flip is a one-line change.

The (B)-finisher, (C), and (C)-descent arguments above are complete proofs (they make explicit the x-parity steps that orig #75's compressed statements left implicit); implement them as stated.

Evidence and output conventions

• Elementary regimes: Evidence(kind="structural", ...) whose text states the exact congruence/descent argument used (including the descent chain D -> D/4 -> ... when applicable), certified=False semantics per evidence.py defaults, completeness="proved", kinds finite-complete/empty.
• Scope, symmetry, tuple order, solvers._verified, and SolutionSet assembly follow Ramanujan–Nagell solver integration and regression fixtures #88; this child only produces the per-regime mathematical content and the structural evidence records.
• No CAS call is made anywhere in this child: every step is exact ZZ arithmetic.

Failure and fallback semantics

• The deferral in step 4 is the only failure path this child owns; its message and outcome are pinned verbatim above.
• No CAS calls are made in the elementary regimes (pure ZZ arithmetic), so no cas-failure arises here.
• No resource-exceeded path exists here either: the recursion depth is floor(v_2(D)/2) and each level performs at most three exact square tests.

Acceptance criteria

Every expected set below is proved complete by the arguments of this issue (plus Nagell's theorem in the routed (7, 1) cases), and each was independently re-verified by exhaustive search on Sage 10.7: k * 2^n - D tested for squareness with exact integer arithmetic for 0 <= n <= 400. The two regime claims of steps 1–3 were also verified exhaustively (Sage 10.7) for all 1 <= D < 400 and all odd 1 <= k < 60 with n <= 300: no solution with n > 2 in the (B)-finisher regime, none with n > 1 in the D ≡ 2 (mod 4) regime, and the n >= 2 part of every D ≡ 0 (mod 4) solution set is exactly the image of ELEM(D/4, k) under (t, n') -> (2t, n' + 2).

• Fixture (7, 1, 2) — routing, and agreement with Nagell. The layer recognizes D ≡ 7 (mod 8), (D, k) = (7, 1) at the top level and returns the hardwired result unchanged; the test asserts the solution set is exactly {(1, 3), (3, 4), (5, 5), (11, 7), (181, 15)} as x > 0 representatives — it must agree with the hardwired Nagell 1961 answer, and the test asserts equality with the fast path's output object conventions (same scope string, same evidence kind).
• Fixture (4, 1, 2) — (C)-descent into the (B)-finisher. solve("x^2 + 4 = 2^n") returns exactly {(0, 2), (2, 3)} as x >= 0 representatives (tuple order (x, n)), completeness="proved"; over ZZ the sign symmetry adds x -> -x (fixing (0, 2)). The hand argument is stated in the test/docstring: n ∈ {0, 1} give 2^n - 4 < 0, impossible; for n >= 2, x is even, x = 2t gives t^2 + 1 = 2^(n-2); if n - 2 >= 2 then t^2 ≡ -1 ≡ 3 (mod 4), impossible; so n - 2 ∈ {0, 1}, i.e. t ∈ {0, ±1}, giving (x, n) ∈ {(0, 2), (±2, 3)}. (This is exactly ELEM(4, 1) -> ELEM(1, 1), case 3 then case 1.)
• Fixture (1, 1, 2) — pure (B)-finisher. Exactly {(0, 0), (1, 1)}.
• Fixture (2, 1, 2) — the D ≡ 2 (mod 4) case. Exactly {(0, 1)}.
• Fixture (28, 1, 2) — descent composed with the classical tail. 28 = 4 * 7 ≡ 0 (mod 4) descends once to (7, 1); expected set exactly {(2, 5), (6, 6), (10, 7), (22, 9), (362, 17)} (the Nagell set transported through (t, m) -> (2t, m + 2), plus empty direct checks at n ∈ {0, 1}).
• Fixture (112, 1, 2) — two descent levels. 112 = 16 * 7 descends twice to (7, 1); expected set exactly {(4, 7), (12, 8), (20, 9), (44, 11), (724, 19)} (the Nagell set transported through (t, m) -> (4t, m + 4)). This fixture locks the composed transport (x, n) = (2^j t, n' + 2j) with j = 2.
• Deferral regression. solve("x^2 + 15 = 2^n") (15 ≡ 7 (mod 8), (D, k) != (7, 1)) raises SolverUnavailable with outcome="unsupported-family" and the verbatim message above. Same for solve("x^2 + 23 = 2^n") (23 ≡ 7 (mod 8)). These two tests are flipped by Ramanujan–Nagell solver integration and regression fixtures #88 when the split machinery lands (the instances then become covered, with sets {(1, 4), (7, 6)} and {(3, 5), (45, 11)} respectively — values recorded here only so the flip is mechanical; Ramanujan–Nagell solver integration and regression fixtures #88 owns them).
• Odd-k split regression. solve("x^2 + 7 = 9*2^n") also stays on the deferral here: 7 ≡ 7 (mod 8) and (D, k) = (7, 9) != (7, 1), so it is not covered by this child even though k is odd. The test asserts the verbatim raise; Ramanujan–Nagell solver integration and regression fixtures #88's flip later asserts kind="empty", completeness="proved" for it (verified: no solution with n <= 400). This case is listed because "k odd" is easy to mistake for "covered".
• Structural evidence serializes (Evidence.to_dict(), as_dict() JSON-serializable with exact tagged values); every returned point passes solvers._verified.
• Every function (private helpers included) has a Sage-convention docstring with INPUT/OUTPUT and EXAMPLES passing sage -t; make test, make doctest, make coverage (docstring coverage stays 100%) all clean.

Out of scope

• The split regime's mathematics (D ≡ 7 (mod 8) beyond routing) — Pethő–de Weger ideal and recurrence branch enumeration #86 (branches) and Explicit analytic bounds and certified reductions for Ramanujan–Nagell #87 (bounds/reduction).
• Dispatch, guards, perfect-power reduction, capabilities, serialization updates, and the k > 1 committed fixture — Ramanujan–Nagell solver integration and regression fixtures #88.
• Any b != 2 regime.