1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
//! The shared inner solver: the **parametric Risch differential equation**
//!
//! ```text
//! R'(x) + θ(x)·R(x) = Σ_{i=0}^{J} a_i·r_i(x)
//! ```
//!
//! over `Q(n)(x)`, solved by undetermined coefficients.
//!
//! # Why one solver serves both stages
//!
//! Dividing the certificate identity `Σ_i a_i(n)·F(n+i,x) = D_x(R·F)` through
//! by `F` turns it into exactly the equation above, with `θ = ∂_x F/F` and
//! `r_i = F(n+i,x)/F(n,x)` — both supplied exactly by
//! [`super::hyperexp::HyperExpTerm`]:
//!
//! ```text
//! D_x(R·F) = (R' + θ·R)·F
//! ```
//!
//! The indefinite case ([`mod@super::dgosper`]) is the same equation with `J = 0`
//! and `a_0` normalised to `1`, i.e. `R' + θ·R = 1`; creative telescoping
//! (`super::search`) is the same equation with `a_0 … a_{J−1}` unknown and
//! `a_J = 1`. Writing two solvers would mean two ansatz shapes, two
//! completeness stories and two places for a certificate to be wrong.
//!
//! # Relationship to `integrate::risch::rational_rde`
//!
//! `integrate::risch::rational_rde::solve_rational_rde_generalized` already
//! solves `v' + f·v = c` over `ℚ(x)` for rational `f`, which is the `J = 0`,
//! `n`-free case of this. It is **not** reused, for two independent reasons,
//! and the first one is a correctness reason:
//!
//! 1. Its denominator bound for `v` is `E = gcd(D, D')` with `D` the
//! denominator of the right-hand side `c` — Bronstein §6.1, which is exact
//! when `f` is a *polynomial*. When `f` has poles, `v` may have poles that
//! `c` knows nothing about. Concretely, `∫ x²·eˣ dx = (x²−2x+2)·eˣ` is the
//! equation `R' + (2/x + 1)·R = 1`, whose solution `R = (x²−2x+2)/x²` has a
//! double pole at `0`, while `c = 1` gives `D = E = 1` and admits only
//! polynomial `v`. That solver returns `None` there — a false refusal for
//! this module's purposes. (Its `f` is `k·η'` in the exponential tower,
//! where the polynomial hypothesis does hold; the gap is in the
//! *generalized* entry point, not in the tower that uses it.)
//! 2. It is over `ℚ`, not `Q(n)`, and the `a_i` unknowns of stage 3 are
//! coupled to the unknown numerator of `R` in one linear system. A
//! standalone RDE solve cannot express that coupling at all.
//!
//! Reusing it as a fast path for the `n`-free case and falling back here would
//! give the same question two answers with two different completeness
//! profiles. One solver, one ansatz, one honest limitation is better.
//!
//! # The ansatz, and exactly how much of it is a guess
//!
//! Write `θ = A/D` (reduced, `D` monic) and let `B` be a common denominator of
//! the `r_i`, so `r_i = ρ_i/B` with `ρ_i ∈ Q(n)[x]`. The ansatz is
//!
//! ```text
//! R = P(x) / (D(x)^κ · B(x)), deg P ≤ d.
//! ```
//!
//! The *support* of that denominator is forced, not guessed. Let `α` be a pole
//! of `R` of order `m ≥ 1` and look at the orders on both sides of the
//! equation at `α`:
//!
//! - `θ` regular at `α`: `R'` has a pole of order `m+1` and `θ·R` at most `m`,
//! so no cancellation is possible and the right-hand side must have a pole of
//! order `m+1` there. So `α` is a pole of some `r_i`, i.e. a root of `B`, and
//! `m ≤ ord_α(B) − 1`.
//! - `θ` with a pole of order `e ≥ 2`: `θ·R` has order `m+e > m+1`, so again no
//! cancellation, `m + e = ord_α(RHS) ≤ ord_α(B)`.
//! - `θ` with a *simple* pole of residue `ρ`: `R'` and `θ·R` both have order
//! `m+1`, with leading coefficients summing to `(ρ − m)·c`. Unless `ρ = m`
//! the same argument applies; when `ρ = m` they cancel and `R` may have a
//! pole of order `m` at a point the right-hand side is regular at.
//!
//! So a pole of `R` lies over a root of `D` or of `B` and nowhere else — which
//! is what `D^κ·B` encodes. What is *not* forced is `κ`: it is exactly the
//! resonance `ρ = m` of the third bullet, and `ρ ∈ Q(n)` is symbolic in the
//! cases this module exists for (`θ = n/x + …` for `F = xⁿ·…`), so whether it
//! occurs is not decidable. `κ` is therefore a bounded search, `d` likewise,
//! and running out of either is [`super::DiffTelescopingError::SearchExhausted`] —
//! never a certificate that was not verified.
//!
//! # The linear system
//!
//! Clearing `Q²·D` out of `Σ_i a_i·r_i = R' + θ·R` with `R = P/Q`,
//! `Q = D^κ·B`, and using `Q²D/B = D^{2κ+1}·B`, gives a *polynomial* identity
//! in `Q(n)[x]` that is linear in the unknowns:
//!
//! ```text
//! Σ_i a_i · (ρ_i · D^{2κ+1} · B) = D·Q·P′ − (D·Q′ − A·Q)·P
//! ```
//!
//! Equating coefficients of each power of `x` is a linear system over the field
//! `Q(n)`, solved by the same Gaussian elimination the discrete engine uses
//! ([`mod@super::super::zeilberger`]'s `field_gaussian_solve`).
use crate;
use cratefield_gaussian_solve;
/// Refuse a probe whose linear system would be larger than this.
///
/// The same protection [`super::super::telescoping2d`]'s `MAX_ANSATZ_UNKNOWNS`
/// provides: the elimination is `O(rows · cols²)` over unbounded-precision
/// rational functions, so a caller who raises the bounds far enough must still
/// not be able to wedge the process. Every worked example in this module stays
/// under 40.
pub const MAX_ANSATZ_UNKNOWNS: usize = 256;
/// The degree-independent part of one order's setup: the shift ratios put over
/// a common denominator, and `θ` split into numerator and denominator.
pub
/// One solved candidate: the recurrence coefficients (with `a_J = 1`) and the
/// certificate. **Not** yet verified — [`verify`] is a separate step on
/// purpose, so that what makes a candidate a result is independent of how the
/// search found it.
pub
/// `x^j` as an element of `Q(n)[x]`.
/// Try one `(κ, d)` probe: solve the linear system for `P` and `a_0..a_{J−1}`
/// with `a_J = 1`.
///
/// `None` means this probe's system has no solution (or was refused as too
/// large), which says nothing at all about neighbouring probes.
pub
/// The **only** thing that makes a candidate a result: check
/// `Σ_i a_i·r_i = R′ + θ·R` as an exact identity in `Q(n)(x)`.
///
/// This re-derives `R′` from `R` and never consults the linear system that
/// produced it, so a bug in the ansatz bookkeeping cannot produce a passing
/// certificate.
pub
/// Scale a solved `(a, R)` pair by a common `x`-free factor `s(n)`.
///
/// Both sides of `Σ_i a_i·r_i = R′ + θ·R` are `Q(n)`-linear and `s` does not
/// depend on `x`, so this preserves the identity exactly. It is how the
/// rational `a_i(n)` become the integer-content-primitive polynomials a caller
/// wants to read as a recurrence — and the scaled pair, not the pre-scaled one,
/// is what [`verify`] is then run on.
pub