Explicit analytic bounds and certified reductions for Ramanujan–Nagell

[roed-math]

Goal

The analytic layer of the generalized Ramanujan–Nagell pipeline: bound #86's branch index q by an explicit initial bound from named theorems — the Bugeaud–Laurent p-adic two-logarithm estimate and Matveev's theorem in the form of [BugeaudMignotteSiksek2006, Thm 9.4] — reduce it with #72's certified p-adic reduction rounds, and hand #88 a terminal exact search box together with the machine-checkable certificate. Pipeline name "ramanujan-nagell-petho-deweger".

No constant in this issue is deferred. The two theorems are transcribed with the source open (WebFetch), every specialization step is written out, and every pinned number was recomputed with certified ball arithmetic on Sage 10.7 — each claim below says which of the three grounds it rests on.

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: Pethő–de Weger ideal and recurrence branch enumeration #86 (the branch records this issue bounds) and Certified logarithmic-bound and LLL-reduction primitives #72 (the certified reduction primitives and the certificate schema).
• Unblocks: Ramanujan–Nagell solver integration and regression fixtures #88.

Supported inputs

One #86 branch record (pattern, A, r, t, tau, mu, u) for an instance in regime (A) or (B-split), together with #86's shared record (d0, f, K, omega, delta, shift s, F, beta). Notation is #86's throughout: alpha = u*tau*mu^q, m = t*q + r, n = m + s, beta = alpha - alphabar = (2/delta)*sqrt(-D), a_p = v_p(b), T = Tr(mu), N = N(mu) = b^t, N(tau) = k*b^r, N(beta) = (2/delta)^2 * D.

Algorithm and conventions

1. The p-adic linear form and its exact decay (proved inline)

Fix a prime p | b. By #86, (p) = Q_p * Qbar_p splits and v_{Q_p}(mu) = t*a_p > 0, v_{Qbar_p}(mu) = 0.

The embedding (pinned, deterministic). K embeds into Q_p because p splits; an embedding is exactly a choice of s := iota(sqrt(-d0)) ∈ Z_p, and there are two, s and -s. Both are computed by simple-root Hensel lifting:

• regime (A): from x^2 + d0, whose roots mod p are simple because p is odd and p ∤ d0;
• regime (B-split), p = 2: x^2 + d0 ≡ (x+1)^2 (mod 2) has a double root, so lift omega = (1 + sqrt(-d0))/2 instead — its minimal polynomial is x^2 - x + (1 + d0)/4, and d0 ≡ 7 (mod 8) makes (1 + d0)/4 even, so mod 2 it is x*(x - 1) with the two simple roots 0, 1 (derivative 2x - 1 ≡ 1); then s := 2*iota(omega) - 1.

Define iota_s(z_0 + z_1*sqrt(-d0)) := z_0 + z_1*s. Exactly one of the two choices gives v_p(iota_s(mu)) = 0 (the other gives t*a_p > 0, because the two embeddings realize Qbar_p and Q_p); iota is that one. It is found by an exact valuation test, so the choice is deterministic.

Under iota: v_p(iota(u)) = 0 (root of unity), v_p(iota(tau)) = v_{Qbar_p}(tau) = 0, and v_p(iota(beta)) = 0 — in regime (A) because beta = 2*sqrt(-D) with p odd and p ∤ D, in regime (B-split) because beta = sqrt(-D) with D odd and p = 2.

Put

eta := iota(u*tau/beta) * iota(mu)^q  =  iota(alpha)/iota(beta)      (a p-adic unit).

Lemma P1 (exact p-adic decay). v_p(eta - 1) = a_p * m = a_p*(t*q + r).

Proof. alpha - beta = alphabar, so eta - 1 = (iota(alpha) - iota(beta))/iota(beta) = iota(alphabar)/iota(beta), whence v_p(eta - 1) = v_p(iota(alphabar)) - 0 = v_{Qbar_p}(alphabar) = v_{Q_p}(alpha) = m*a_p, the last equality by #86's Lemma SPLIT ((alpha) = A*C^m with A coprime to (b)). ∎

Lemma P2 (multiplicative form to linear form). For a p-adic unit eta ∈ Z_p^* and log_p the standard p-adic logarithm on units (the extension that kills the Teichmüller part — Sage's .log(); verified on Sage 10.7 that Qp(3,40)(-1).log(), Qp(3,40).teichmuller(7).log() and Qp(2,40)(-1).log() are all zero):

v_p(log_p(eta)) >= v_p(eta - 1),

with equality whenever v_p(eta - 1) >= 1 (p odd) or >= 2 (p = 2).

Proof. If p is odd and eta ≢ 1 (mod p) then v_p(eta - 1) = 0 and the inequality is trivial. If eta ≡ 1 (mod p^sigma) with sigma >= 1 (p odd) or sigma >= 2 (p = 2), then log_p(eta) = sum_{j>=1} (-1)^(j+1) (eta-1)^j / j converges and v_p((eta-1)^j/j) = j*sigma - v_p(j) > sigma for j >= 2 (because (j-1)*sigma - v_p(j) >= (j-1) - log_p(j) > 0 for p >= 3, resp. 2*(j-1) - log_2(j) > 0 for p = 2), so v_p(log_p eta) = sigma. The one remaining case is p = 2, v_2(eta - 1) = 1: then eta ≡ 3 (mod 4), log_2(eta) = (1/2)*log_2(eta^2) and v_2(eta^2 - 1) = v_2(eta-1) + v_2(eta+1) >= 1 + 2 = 3, so v_2(log_2 eta) >= 2 > 1. ∎

(Machine check, Sage 10.7: Qp(2,40)(3).log().valuation() == 2 while (Qp(2,40)(3) - 1).valuation() == 1 — the inequality is strict exactly in that case. For the (7,1,2) branches, v_2(eta-1) equals m at every solution index and v_2(log_2 eta) equals it too for m >= 2, being 4 at m = 1.)

The linear form. Since log_p is a homomorphism on units and iota(beta)^2 = beta^2 ∈ ZZ with v_p(beta^2) = 0,

Lambda := log_p(eta) = delta_p + q * mu_1,
mu_1   := log_p(iota(mu)),
delta_p := log_p(iota(u*tau)) - (1/2) * log_p(beta^2).

Decay record for #72. By P1 + P2, every q >= 0 of the branch satisfies

v_p(Lambda) >= a_p*(t*q + r) >= (a_p*t) * q,

so the branch supplies PadicDecay(kappa = ZZ(a_p*t), c0 = QQ(0)) with height H := q. There is no absorbed exception set: the inequality holds for every counted solution, including the small-q ones where P2 is strict.

2. Representing the form in #72's pinned p-adic grammar

reduce_linear_form accepts mus/delta entries that are ZZ/QQ, PadicAlgebraic(minpoly, residue), or PadicLogValue(constant, log_terms). This family's form maps in exactly:

M      = PadicAlgebraic(minpoly=(N, -T, 1), residue=ZZ(T % p))          # iota(mu)
mus    = (PadicLogValue(QQ(0), ((QQ(1), M),)),)                          # mu_1
delta  = PadicLogValue(QQ(0), ((QQ(1), U), (QQ(-1)/2, QQ(beta**2))))     # delta_p

• M is always legal. x^2 - T*x + N is monic over ZZ; p | N = b^t, so mod p it is x*(x - T), and T ≢ 0 (mod p) by Pethő–de Weger ideal and recurrence branch enumeration #86 §5. Hence residue = T mod p is a root, it is simple (f'(residue) = 2T - T = T ≢ 0), and it is nonzero — so M is a unit, as PadicLogValue requires. (Verified on Sage 10.7 for every branch of the fixtures: (7,1,2) x^2 - x + 2, residue 1; (5,1,3) x^2 + 4x + 9, residue 2; (14,9,5) x^2 - 22x + 625, residue 2.)
• U represents iota(u*tau). If u*tau ∈ QQ take U := QQ(u*tau), a p-adic unit — this is the case in the (7,1,2) and (5,1,3) fixtures, where tau = 1 and U = ±1 (and log_p(±1) = 0). Otherwise U := PadicAlgebraic(minpoly=(N(u*tau), -Tr(u*tau), 1), residue=rho) with rho the residue of iota(u*tau) — this is the case in the (2,2,3) fixture, where tau = sqrt(-2), the minimal polynomial is x^2 + 2 (tuple (2, 0, 1)) and rho ∈ {1, 2} depending on the branch; mod 3 that polynomial is (x-1)*(x+1) with both roots simple (f'(x) = 2x ≢ 0), so the record is legal (verified on Sage 10.7: the four branches give rho = 1, 2, 2, 1).
• Normalization N1 (always makes U legal). If rho is not a simple root of that minimal polynomial mod p (possible only when r = 0, since r >= 1 forces p | N(tau)), replace the branch parametrization alpha = (u*tau)*mu^q by alpha = (u*tau*mu)*mu^(q-1) and use the index q* := q - 1 >= 0, checking q = 0 (i.e. n = r + s) directly. Then v_{Q_p}(tau*mu) = (r + t)*a_p >= 1 and v_{Qbar_p}(tau*mu) = 0, so p | N(u*tau*mu), the roots mod p are 0 and Tr(u*tau*mu), and they are distinct — otherwise both would be ≡ 0 (mod p), i.e. both iota(u*tau*mu) and its conjugate would have positive valuation, contradicting v_{Qbar_p}(tau*mu) = 0. The element is also irrational for the same reason, so the degenerate QQ case cannot arise. The decay is unaffected: v_p(Lambda) >= a_p*(t*(q*+1) + r) >= (a_p*t)*q*. ∎
• beta^2 = -(2/delta)^2 * D ∈ ZZ and v_p(beta^2) = 0, so it is a legal QQ log argument.
• Dimension. n = 1 (a single exponent unknown q), inhomogeneous (delta_p is a symbolic PadicLogValue, hence treated inhomogeneously by Certified logarithmic-bound and LLL-reduction primitives #72's rule). Both branches of Certified logarithmic-bound and LLL-reduction primitives #72's Lemma P-inh are live: if v_p(delta_p) < m0 := v_p(mu_1) the degenerate branch applies and returns X1 = floor((v_p(delta_p) + c0)/kappa) with no lattice at all; otherwise the main branch below runs. (Verified on Sage 10.7 that all three committed fixtures take the main branch, with (m0, v_p(delta_p)) equal to (2, 2), (1, 1) and (1, 1) respectively on every branch.) Certified logarithmic-bound and LLL-reduction primitives #72's construction then degenerates to Gamma_nu = p^nu * ZZ and Lemma P-inh reads: if the residue d^(nu) of d = delta_p/mu_1 satisfies ell_y = min(d^(nu), p^nu - d^(nu)) > X0, then v_p(Lambda) <= m0 + nu - 1, hence X1 = floor((m0 + nu - 1 + c0)/kappa) = floor((m0 + nu - 1)/(a_p*t)). This is exactly the classical p-adic reduction (compare enough p-adic digits of delta_p/mu_1 against the box); the degeneration is the intended use, not a misuse of the primitive.
• Precision. Certified logarithmic-bound and LLL-reduction primitives #72's p-adic digit convention: at bit precision b, build Q_p with the least k such that p^k >= 2^b. At the starting b = 128 this is k = 128 for p = 2, 81 for p = 3, 56 for p = 5, 46 for p = 7 (verified on Sage 10.7). All rounds of the committed fixtures certify at precision_bits = 128.
• max_precision_bits is passed through from Ramanujan–Nagell solver integration and regression fixtures #88 and defaults to 1 << 16, exactly Certified logarithmic-bound and LLL-reduction primitives #72's default. No other resource knob exists.

3. The archimedean linear form and its exact decay (proved inline)

Lambda_arch := zeta * (mubar/mu)^q - 1,        zeta := (ubar*taubar)/(u*tau).

Derivation. alpha - alphabar = beta; dividing by alpha gives 1 - alphabar/alpha = beta/alpha, and alphabar/alpha = zeta*(mubar/mu)^q, so Lambda_arch = -beta/alpha. Hence, with |u| = 1, |mu| = b^(t/2) and |tau| = sqrt(k*b^r) (#86 §5),

|Lambda_arch| = |beta| / (|tau| * |mu|^q) = K1 * exp(-K2 * q),
K1 := sqrt( N(beta) / (k*b^r) )  ∈ AA,          K2 := (t/2) * log b.

This is an equality, so the RealDecay(K1, K2) contract holds for every q with no exception set. Lambda_arch != 0 because beta != 0 (D >= 1) — this is the non-vanishing hypothesis of Theorem 9.4 below, discharged unconditionally.

Exact heights on the unit circle. For gamma ∈ K with |gamma| = 1, h(gamma) = (1/2)*log(a_0(gamma)) where a_0(gamma) is the leading coefficient of the primitive integral minimal polynomial of gamma (and a_0 = 1, h = 0, when gamma = ±1). Proof: all conjugates have modulus 1, so the log^+ terms of the Weil height vanish and h = (1/deg)*log a_0, with deg ∈ {1, 2} matching. ∎

a_0(mubar/mu) = b^t, i.e. h(mubar/mu) = (t/2)*log b. Proof: mubar/mu satisfies N*x^2 - (T^2 - 2N)*x + N = 0 with N = b^t; this is primitive because gcd(N, T^2 - 2N) = gcd(N, T^2) = 1, which follows from p ∤ T for every p | b (#86 §5). ∎ (Verified on Sage 10.7 for every branch of the fixtures: a_0 = 2, 9, 3 for (7,1,2), (5,1,3), (2,2,3).)

4. Matveev's theorem in the form of [BugeaudMignotteSiksek2006, Thm 9.4] — transcribed and specialized

The theorem (transcribed from the source). Matveev's lower bound in the form of Bugeaud–Mignotte–Siksek (BugeaudMignotteSiksek2006, already in data/references.bib), Classical and modular approaches to exponential Diophantine equations. I. Fibonacci and Lucas perfect powers, Section 9.1; transcribed faithfully from the arXiv text (arXiv:math/0403046) with the source open — ground: fetched and transcribed, not restated from memory. Setup, quoted with only notational reflow:

Let L be a number field of degree D, let alpha_1, ..., alpha_n be non-zero elements of L and b_1, ..., b_n be rational integers. Set B = max{|b_1|, ..., |b_n|} and

Lambda = alpha_1^{b_1} * ... * alpha_n^{b_n} - 1.

Let h denote the absolute logarithmic height and let A_1, ..., A_n be real numbers with A_j >= h'(alpha_j) := max{ D*h(alpha_j), |log alpha_j|, 0.16 } for 1 <= j <= n (h' is the modified height with respect to L).

Theorem 9.4. Assume that Lambda is non-zero. We then have

log |Lambda| > -3 * 30^(n+4) * (n+1)^5.5 * D^2 * (1 + log D) * (1 + log(n*B)) * A_1 * ... * A_n.

Furthermore, if L is real, we have

log |Lambda| > -1.4 * 30^(n+3) * n^4.5 * D^2 * (1 + log D) * (1 + log B) * A_1 * ... * A_n.

The theorem bounds the multiplicative form alpha_1^{b_1}...alpha_n^{b_n} - 1, which is exactly Lambda_arch, so no exp-versus-log comparison enters this stage.

Which inequality applies. L = K is imaginary quadratic, so L is not real: the second (real-field, 1 + log B) inequality is unavailable here, and the specialization uses the first one, with the (1 + log(n*B)) factor. (This is the only point where this family's specialization differs structurally from #73's and #81's, which work over real fields.)

Specialization (every step explicit). L = K, D = [K:QQ] = 2, and:

• Pinned shape rule (deterministic). If zeta = 1 (an exact test in K) take n = 1, alpha_1 = mubar/mu, b_1 = q. Otherwise take n = 2, alpha_1 = mubar/mu, alpha_2 = zeta, (b_1, b_2) = (q, 1). In both cases B = max{|b_i|} = q for q >= 1 (q = 0 is checked directly).

• Admissible heights. For gamma on the unit circle, h'(gamma) = max{2*h(gamma), |log gamma|, 0.16} = max{log a_0(gamma), |arg gamma|, 0.16} and |arg gamma| <= pi, so the following are admissible and avoid computing any argument:

  A_1 := max{ t*log b, pi }          (>= max{2*h(mubar/mu), |arg|, 0.16},  using 2*h = log(b^t))
  A_2 := max{ log a_0(zeta), pi }    (>= max{2*h(zeta),    |arg|, 0.16})
  

• Leading constant. C_arch := 3 * 30^(n+4) * (n+1)^5.5 * 4 * (1 + log 2) * A_1 * ... * A_n. For n = 2 the numeric part is 3 * 30^6 * 3^5.5 * 4 * (1 + log 2) = 6.2340515198646158...e12 (certified 256-bit ball enclosure, Sage 10.7).

• The inequality. log|Lambda_arch| = log K1 - K2*q by §3, so Theorem 9.4 gives, for every solution with q >= 1,

  K2*q - log K1 < C_arch * (1 + log(n*q)).
  

Closing the implicit inequality (pinned closure; proved inline). Put g(X) := K2*X - log K1 - C_arch*(1 + log(n*X)) for X >= 1.

• Monotonicity lemma. g'(X) = K2 - C_arch/X > 0 for X > C_arch/K2, so g is strictly increasing on [C_arch/K2, oo). If an integer X* >= C_arch/K2 has g(X*) > 0, then every real q >= X* has g(q) > 0, so no solution has q >= X*, i.e. every solution has q <= X* - 1. ∎
• Certified test. CERT(X) := [upper(ball(C_arch/K2)) <= X] and [lower(ball(g(X))) > 0], evaluated in RealBallField(256) — the working precision of this closure is pinned at 256 bits — with the endpoints compared exactly against the integer X. Ball endpoints are always valid bounds, so low precision can only make CERT conservatively false, never wrong; the pinned precision makes the returned value deterministic.
• Algorithm. Doubling: test X = 2, 4, 8, ... until the first X = 2^k with CERT(X); then bisect (lo := 2^(k-1), hi := 2^k; while hi - lo > 1: mid := floor((lo+hi)/2); if CERT(mid) then hi := mid else lo := mid), and return N_BMS := hi - 1. CERT is monotone in X on the certified range (both conjuncts are), so the bisection is valid.

5. The Bugeaud–Laurent p-adic two-logarithm bound — transcribed and specialized

The theorem (transcribed from an open restatement). BugeaudLaurent1996 — Yann Bugeaud, Michel Laurent, Minoration effective de la distance p-adique entre puissances de nombres algébriques, Journal of Number Theory 61 (1996), 311–342 — is paywalled. The statement below is Corollary 1 of that paper as restated verbatim in István Pink and Volker Ziegler, Effective Resolution of Diophantine equations of the form u_n + u_m = w p_1^{z_1} ... p_s^{z_s}, arXiv:1604.04720, their Theorem 2 ("let us state a result due to Bugeaud and Laurent [6, Corollary 1]"); ground: fetched (ar5iv HTML) and transcribed with the source open, not restated from memory. The bibliographic data of the original was cross-checked against Tomohiro Yamada, A note on the paper by Bugeaud and Laurent "Minoration effective de la distance p-adique entre puissances de nombres algébriques", arXiv:math/0607072, whose reference [1] reads exactly "Y. Bugeaud and M. Laurent, Minoration effective de la distance p-adique entre puissances de nombres algébriques, J. Number Theory 61 (1996), 311–342". Cite both: the original for the result, the restatement for the wording actually used.

Setup, quoted with only notational reflow (nu_p is the p-adic valuation, h the absolute logarithmic Weil height):

Let p be a prime, L = QQ_p(alpha_1, alpha_2), and let f be the residual degree of that extension. Put Dcal = [QQ(alpha_1, alpha_2) : QQ] / f, and let h'(alpha_i) >= max{h(alpha_i), log p / Dcal} for i = 1, 2.

Theorem (Bugeaud–Laurent, Corollary 1). Let b_1, b_2 be positive integers and suppose that alpha_1 and alpha_2 are multiplicatively independent algebraic numbers such that nu_p(alpha_1) = nu_p(alpha_2) = 0. Put b' := b_1/(Dcal*h'(alpha_2)) + b_2/(Dcal*h'(alpha_1)). Then

nu_p(alpha_1^{b_1} * alpha_2^{b_2} - 1)
    <=  24*p*(p^f - 1)*Dcal^4 / ((p - 1) * (log p)^4)  *  B^2 * h'(alpha_1) * h'(alpha_2),
B := max{ log b' + log log p + 0.4,  10,  10*log p/Dcal }.

Note on the floor 10. Some restatements of the same corollary carry a smaller third entry in the max. Using the larger floor can only increase the right-hand side, so the conclusion stays valid; this issue uses the floor it actually read, max{..., 10, 10 log p/Dcal}, and the derived bounds are therefore conservative.

Specialization (every step explicit). Take alpha_1 = mu, b_1 = q >= 1, alpha_2 = u*tau/beta, b_2 = 1, so alpha_1^{b_1} alpha_2^{b_2} - 1 = eta - 1 of §1 (both are p-adic units under iota, i.e. nu_p(alpha_i) = 0).

• f = 1 and Dcal = 2. p splits in K, so iota embeds K into QQ_p and L = QQ_p, giving residual degree f = 1. mu is irrational (its two Q_p-embeddings have different valuations), so QQ(alpha_1, alpha_2) = K has degree 2, and Dcal = 2/1 = 2.

• Leading constant collapses. With f = 1, (p^f - 1) = (p - 1) cancels the denominator's (p - 1) and Dcal^4 = 16, so

  24*p*(p^f - 1)*Dcal^4 / ((p-1)*(log p)^4)  =  384 * p / (log p)^4.
  

• Heights (exact). For an algebraic integer gamma of an imaginary quadratic field, both conjugates have modulus sqrt(N(gamma)), so h(gamma) = (1/2)*log N(gamma). Hence h(mu) = (t/2)*log b and h(u*tau/beta) <= h(u*tau) + h(beta) = (1/2)*log(k*b^r) + (1/2)*log N(beta). Take the smallest admissible choices

  h'(alpha_1) := max{ (t/2)*log b,                  (log p)/2 },
  h'(alpha_2) := max{ (1/2)*log(k*b^r*N(beta)),     (log p)/2 }.
  

  (When tau = 1 — all three committed fixtures — the second is exactly max{(1/2) log N(beta), (log p)/2}.)

• Multiplicative independence (exact test, no heuristics). Let S be the set of primes of O_K in the supports of the fractional ideals (mu) and (u*tau)*(beta)^(-1), and form the 2 x |S| integer matrix of their valuations. Then alpha_1, alpha_2 are multiplicatively independent iff that matrix has rank 2. Proof: rank 2 forbids any nonzero (c_1, c_2) with (alpha_1)^{c_1}(alpha_2)^{c_2} = (1), hence any multiplicative relation. Conversely, if the rank is <= 1, a nonzero integer kernel vector (c_1, c_2) makes alpha_1^{c_1} alpha_2^{c_2} a unit of O_K; K is imaginary quadratic, so every unit is a root of unity, and raising to the power w = |O_K^*| gives a genuine relation. ∎ (Verified rank 2 for every branch of the three committed fixtures.)

• The inequality. With Lemma P1 (nu_p(eta - 1) = a_p*(t*q + r) >= a_p*t*q), every solution of the branch satisfies

  a_p*t*q  <=  (384*p/(log p)^4) * h'(alpha_1) * h'(alpha_2) * B(q)^2,
  b'(q) = q/(2*h'(alpha_2)) + 1/(2*h'(alpha_1)),
  B(q)  = max{ log b'(q) + log log p + 0.4,  10,  5*log p }.
  

• Closure. Identical to §4: g_p(X) := a_p*t*X - (384*p/(log p)^4)*h'(alpha_1)*h'(alpha_2)*B(X)^2 is eventually strictly increasing (B(X)^2 grows like (log X)^2), the same CERT/doubling/bisection procedure at 256 bits returns N_BL(p) := hi - 1, and every solution has q <= N_BL(p).

6. The initial bound, the reduction chain, and the terminal search

N_0 := min( N_BMS,  min over p | b with MI certified of N_BL(p) )

recorded per branch as initial_bound = {"theorem": str, "value": ZZ(N_0)} in #72's schema. The theorem string is pinned: "Bugeaud-Laurent 1996 (p-adic two-log, p = 2)" (with the realizing prime substituted for 2) when a p-adic bound realizes the minimum, and "Matveev (BMS Thm 9.4)" — the same string #73 uses — when the archimedean one does. If multiplicative independence fails for every p | b, the archimedean bound alone is used — Theorem 9.4 needs only Lambda_arch != 0, which §3 proves unconditionally, so no branch is ever left without an initial bound.

Reduction rounds. For a fixed p | b (the smallest one, deterministic) and each branch:

next_round(X) -> reduce_linear_form(mus, delta, X, decay=PadicDecay(ZZ(a_p*t), QQ(0)),
                                    p=p, max_precision_bits=max_precision_bits)
final_bound, evidence = certify_bound_chain(
    "ramanujan-nagell-petho-deweger", initial_theorem, ZZ(N_0), next_round,
    max_precision_bits=max_precision_bits)

• The chain stops when a round fails to strictly decrease the bound (Certified logarithmic-bound and LLL-reduction primitives #72's rule).
• Precision-failure handling (pinned). If reduce_linear_form raises SolverUnavailable(..., outcome="resource-exceeded"), next_round returns None: the chain then stops at the last certified bound, which is sound because every recorded round already certified. The failure is only propagated when no round certified and the initial bound exceeds the terminal-search cap below.
• Terminal-search cap (pinned). _RN_TERMINAL_CAP = 10**4, applied to the terminal search box N_max computed below (equivalently, to max_branches(t*X_final + r) + s). If it is exceeded, raise SolverUnavailable(..., outcome="resource-exceeded") — never a partial answer. Justification: the terminal search is one exact is_square per exponent; measured on Sage 10.7, searching n <= 5000 costs 0.01 s for b = 2 and 0.02 s for b = 3, so 10^4 is comfortably inside the interactive budget while an unreduced ~10^5 bound is not the failure mode we want to hide.
• Terminal exact search. N_max := max over branches of (t*X_final + r) + s; enumerate 0 <= n <= N_max, compute T = k*b^n - D, accept (ZZ(T).isqrt(), n) iff T >= 0 and ZZ(T).is_square(). Exact integer arithmetic only — no recurrence evaluation and no logarithms at this stage. Completeness of this search over the box, together with the certified per-branch bounds, is the completeness proof.

Certificate (exactly #72's schema). One Evidence(kind="certificate", certified=True, software="sage", version=software_version("sage"), certificate={...}) per branch, with

• "pipeline": "ramanujan-nagell-petho-deweger",
• "initial_bound": {"theorem": str, "value": ZZ} with the pinned theorem string above,
• "rounds": one dict per reduction round with exactly the five keys {"dimension", "scaling_C", "precision_bits", "b1_norm_lower", "new_bound"} — here dimension = ZZ(1), scaling_C = ZZ(p)^nu, precision_bits = the Certified logarithmic-bound and LLL-reduction primitives #72 bit precision that certified the round (ZZ(128) in every committed round below; Certified logarithmic-bound and LLL-reduction primitives #72's b is a bit precision, not this family's base b), b1_norm_lower = ZZ(ell_y) (an integer in dimension 1, so Certified logarithmic-bound and LLL-reduction primitives #72's isqrt construction returns it exactly), new_bound = ZZ(X1),
• "final_box": {roles["n"]: [ZZ(r + s), ZZ(t*X_final + r + s)]} — the branch only produces n ≡ r + s (mod t),

plus one Evidence(kind="search-exhaustion", ...) for the terminal search over 0 <= n <= N_max. Every in-memory numeric leaf is an exact Sage ZZ/QQ; nothing is pre-stringified and nothing is coerced through int(...). Evidence.to_dict() performs the tagged serialization (#72's exactness rule), e.g. the first round of the (7,1,2) chain serializes as

{
  "dimension": {"type": "integer", "value": "1"},
  "scaling_C": {"type": "integer", "value": "524288"},
  "precision_bits": {"type": "integer", "value": "128"},
  "b1_norm_lower": {"type": "integer", "value": "161779"},
  "new_bound": {"type": "integer", "value": "20"}
}

Why there is no p=None round. RealDecay(K1, K2) is fully expressible in #72's real grammar (K1 ∈ AA is a quadratic surd, K2 = ExactLogValue(0, ((t/2, b),))), and §3 proves the contract; it is written out above for the record. But the archimedean linear form of this family is an argument form arg(zeta) + q*arg(mubar/mu) - 2*pi*y, whose coefficients are arguments and pi — neither is a ZZ/QQ, an AA, nor a logarithm of a positive rational/real-algebraic number, so they are outside #72's pinned ExactReal grammar. This issue therefore uses the archimedean side for the initial bound only and performs every certified reduction round p-adically. No change to #72's API is requested or implied.

Failure and fallback semantics

• Precision cap reached with no certified round and an initial bound above _RN_TERMINAL_CAP: SolverUnavailable(..., outcome="resource-exceeded") propagates. This family has no bounded partial path today and this child does not add one.
• Terminal search box N_max above _RN_TERMINAL_CAP: the same typed failure.
• CAS failures inside the exact algebraic or p-adic computations surface as outcome="cas-failure" per the existing vocabulary.
• A wrong or silently weakened bound is never an acceptable outcome: every bound recorded is the conclusion of a lemma of this issue or of Certified logarithmic-bound and LLL-reduction primitives #72 whose hypotheses were verified with certified arithmetic.

Acceptance criteria

All numbers below were computed with certified RealBallField(256) / exact Q_p arithmetic on Sage 10.7 from exactly the pinned specializations above, and the resulting solution sets were cross-checked against exhaustive search.

• Fixture (D, k, b) = (7, 1, 2), p = 2 (regime B-split, zeta = 1, so BMS uses n = 1). h'(alpha_1) = (log 2)/2 = 0.34657359027997265..., h'(alpha_2) = (log 7)/2 = 0.97295507452765665..., A_1 = pi, K1 = sqrt(7), K2 = (log 2)/2, kappa = a_p*t = 1, m0 = v_2(log_2(iota(mu))) = 2. Bounds: N_BL(2) = 141414, N_BMS = 6167268621319, so N_0 = 141414 with initial_bound["theorem"] = "Bugeaud-Laurent 1996 (p-adic two-log, p = 2)". Certified chain, identical on all four branches:

  round	dimension	scaling_C	precision_bits	b1_norm_lower	new_bound
  1	1	2^19 = 524288	128	161779	20
  2	1	2^12 = 4096	128	2035	13

  A third round returns 13 (no strict decrease), so the chain stops at q <= 13, final_box n ∈ [2, 15], and the terminal exact search over 0 <= n <= 15 returns exactly {(1, 3), (3, 4), (5, 5), (11, 7), (181, 15)} — it must agree with the hardwired Nagell 1961 answer, and the test asserts that equality.

• Fixture (D, k, b) = (5, 1, 3), p = 3 (regime A, class number 2, t = 2, zeta = 1). h'(alpha_1) = log 3 = 1.09861228866810969..., h'(alpha_2) = (log 20)/2 = 1.49786613677699550..., A_1 = pi, K1 = 2*sqrt(5), K2 = log 3, kappa = 2, m0 = 1. Bounds: N_BL(3) = 73051, N_BMS = 1869287767761, N_0 = 73051. Certified chain (identical on all four branches): round 1 scaling_C = 3^12 = 531441, b1_norm_lower = 150500, new_bound = 6; round 2 scaling_C = 3^5 = 243, b1_norm_lower = 83, new_bound = 2; precision_bits = 128 in both. Final q <= 2, final_box n ∈ [0, 4], terminal search returns exactly {(2, 2)}.

• Fixture (D, k, b) = (2, 2, 3), p = 3 (regime A, k > 1, tau = sqrt(-2) != 1, zeta = -1 != 1, so BMS uses n = 2). h'(alpha_1) = (log 3)/2 = 0.54930614433405485..., and h'(alpha_2) = (1/2)*log(k*b^r*N(beta)) = (1/2)*log(2*8) = log 4 = 1.38629436111989062... (note N(tau) = k*b^r = 2 here, since tau = sqrt(-2)), A_1 = A_2 = pi, K1 = sqrt(N(beta)/(k*b^r)) = sqrt(8/2) = 2, K2 = (log 3)/2, kappa = 1, m0 = 1. Bounds: N_BL(3) = 67610, N_BMS = 4219591963378272, N_0 = 67610. Certified chain (identical on all four branches): round 1 scaling_C = 3^12 = 531441, b1_norm_lower = 192542, new_bound = 12; round 2 scaling_C = 3^5 = 243, b1_norm_lower = 86, new_bound = 5; precision_bits = 128 in both. Final q <= 5, final_box n ∈ [0, 5], terminal search returns exactly {(0, 0), (2, 1), (4, 2), (22, 5)}. This fixture is the one that exercises the n = 2 archimedean specialization and a non-trivial tau.

• Review-then-lock discipline (as in Certified logarithmic-bound and LLL-reduction primitives #72/Proved completion for fixed-base Pillai equations #73): the specializations of §§4–5 are the reviewed object; the chains above are the regression lock. Before the golden certificates are committed, an independent reviewer re-derives Lemmas P1, P2, the height identities of §3, and both specializations from this issue's text and records the sign-off in the implementing PR. The committed round records then come from the implementation's own first verified run, where verified means the terminal search of the produced box reproduces the expected solution set exactly.

• Precision-failure path: a test calls the branch reduction with a tiny cap (e.g. max_precision_bits=32) on an instance whose initial bound exceeds _RN_TERMINAL_CAP and asserts SolverUnavailable with as_dict()["outcome"] == "resource-exceeded".

• Grammar-conformance test: assert that the constructed mus/delta are exactly the pinned PadicLogValue/PadicAlgebraic records, that M's residue is a simple root mod p, and that Normalization N1 fires (and produces a legal U) on a synthetic branch whose u*tau residue is a double root.

• Multiplicative-independence test: assert rank 2 for the three committed fixtures, and assert that a synthetic rank-1 pair routes the initial bound to "Matveev (BMS Thm 9.4)" without raising.

• Bibliography: add BugeaudLaurent1996 to data/references.bib — Yann Bugeaud, Michel Laurent, Minoration effective de la distance p-adique entre puissances de nombres algébriques, Journal of Number Theory, volume 61, 1996, pages 311–342 (REQUIRED_FIELDS author/title/year all pinned, with journal, volume, pages; no url — the article is paywalled and no legally free copy is known, and the restatement actually read is cited in this issue's text, not as a bibliography substitute. An optional doi may be added only if verified at commit time by tools/check_references.py with network access.) Add to the ramanujan-nagell family YAML: BugeaudLaurent1996 with why = "the effective p-adic two-logarithm lower bound supplying the initial exponent bound", and BugeaudMignotteSiksek2006 with why = "Matveev's theorem in the form of Theorem 9.4, the archimedean initial bound". make references and make registry-docs must pass.

• Certificates serialize (Evidence.to_dict(), SolutionSet.as_dict() JSON-serializable with exact tagged values, schema_version unchanged); tests/test_solver_contract.py passes.

• 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 branch enumeration itself — Pethő–de Weger ideal and recurrence branch enumeration #86.
• Dispatch, guards, scope/symmetry, capabilities, serialization wiring, and the user-visible fixtures — Ramanujan–Nagell solver integration and regression fixtures #88.
• The elementary b = 2 regimes — Elementary b = 2 Ramanujan–Nagell branches #85.
• Any change to Certified logarithmic-bound and LLL-reduction primitives #72's API, grammar, or lemma set; any archimedean (p=None) reduction round for this family (see §6); any new resource-budget abstraction beyond max_precision_bits and the pinned _RN_TERMINAL_CAP.